Используя типичное определение naturals типового уровня, я определил 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 rs) = Dimension (map f ls) (f mid) (map f rs)
instance Functor (U n) where
fmap f (Point x) = Point (f x)
fmap f [email protected]{} = dmap (fmap f) d
Теперь я хочу сделать его экземпляром Comonad, но я не могу полностью обернуть вокруг него мозг.
class Functor w => Comonad w where
(=>>) :: w a -> (w a -> b) -> w b
coreturn :: w a -> a
cojoin :: w a -> w (w a)
x =>> f = fmap f (cojoin x)
cojoin xx = xx =>> id
instance Comonad (U n) where
coreturn (Point x) = x
coreturn (Dimension _ mid _) = coreturn mid
-- cojoin :: U Z x -> U Z (U Z x)
cojoin (Point x) = Point (Point x)
-- cojoin ::U (S n) x -> U (S n) (U (S n) x)
cojoin [email protected]{} = undefined
-- =>> :: U Z x -> (U Z x -> r) -> U Z r
[email protected]{} =>> f = Point (f p)
-- =>> :: U (S n) x -> (U (S n) x -> r) -> U (S n) r
[email protected]{} =>> f = undefined
Используя cojoin на n-мерной сетке, будет создана n-мерная сетка n-мерных сеток. Я хотел бы предоставить экземпляр с той же идеей, что и этот, который заключается в том, что значение объединенной сетки в (x, y, z) должна быть исходная сетка, ориентированная на (x, y, z). Чтобы адаптировать этот код, нам кажется, что нам нужно reify n для выполнения n "fmaps" и n "rolls". Вам не обязательно это делать, но если это поможет, тогда вы идете.
