相关疑难解决方法(0)

使用类型级自然的典型定义,我已经定义了一个n维网格.

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}

data Nat = Z | S Nat

data U (n :: Nat) x where
  Point :: x -> U Z x
  Dimension :: [U n x] -> U n x -> [U n x] -> U (S n) x

dmap :: (U n x -> U m r) -> U (S n) x -> U (S m) r
dmap f (Dimension ls mid …