{-# LANGUAGE DataKinds, KindSignatures, PolyKinds, TypeFamilies, GADTs, StandaloneDeriving #-}
Hi. I've tried to implement type-level list myself (as an exercise, not looking into existing libraries): Here are two variants of singletons:
data SList1 :: [*] -> * where SNil1 :: SList1 '[] SCons1 :: a -> SList1 t -> SList1 ('(:) a t)
data SList2 (a :: *) (t :: [*]) :: * where SNil2 :: SList2 a '[] SCons2 :: a -> SList2 a t -> SList2 a ('(:) a t) deriving instance Show a => Show (SList2 a b)
and `map` for type lists:
type family MapF (b :: r) (t :: [k]) :: [r] where MapF b '[] = '[] MapF b ('(:) a t) = ('(:) b (MapF b t))
Then i can write `map` on second singleton variant:
mapF2 :: (a -> b) -> SList2 a t -> SList2 b (MapF b t) mapF2 f SNil2 = SNil2 mapF2 f (SCons2 x xs) = SCons2 (f x) (mapF2 f xs)
but it does not type-check on first: mapF1 :: (a -> b) -> SList1 t -> SList1 (MapF b t) mapF1 f SNil1 = SNil1 mapF1 f (SCons1 x xs) = SCons1 (f x) (mapF1 f xs) because (as i understand) ghc can't deduce from type-signature, that list element type `a` should match type `a` of first map function's argument: Could not deduce (a1 ~ a) from the context (t ~ (a1 : t1)) bound by a pattern with constructor SCons1 :: forall a (t :: [*]). a -> SList1 t -> SList1 (a : t), in an equation for ‘mapF1’ at 1.lhs:37:12-22 ‘a1’ is a rigid type variable bound by a pattern with constructor SCons1 :: forall a (t :: [*]). a -> SList1 t -> SList1 (a : t), in an equation for ‘mapF1’ at 1.lhs:37:12 ‘a’ is a rigid type variable bound by the type signature for mapF1 :: (a -> b) -> SList1 t -> SList1 (MapF b t) at 1.lhs:35:12 Relevant bindings include x :: a1 (bound at 1.lhs:37:19) f :: a -> b (bound at 1.lhs:37:9) mapF1 :: (a -> b) -> SList1 t -> SList1 (MapF b t) (bound at 1.lhs:36:3) In the first argument of ‘f’, namely ‘x’ In the first argument of ‘SCons1’, namely ‘(f x)’ Then i try to bind these types using different type family definition:
type family MapF' (a :: k) (b :: r) (t :: [k]) :: [r] where MapF' a b '[] = '[] MapF' a b ('(:) a t) = ('(:) b (MapF' a b t))
but ghc still can't deduce type equality: mapF1' :: (a -> b) -> SList1 t -> SList1 (MapF' a b t) mapF1' f SNil1 = SNil1 mapF1' f (SCons1 x xs) = SCons1 (f x) (mapF1' f xs) Could not deduce (a1 ~ a) from the context (t ~ (a1 : t1)) bound by a pattern with constructor SCons1 :: forall a (t :: [*]). a -> SList1 t -> SList1 (a : t), in an equation for ‘mapF1'’ at 1.lhs:72:13-23 ‘a1’ is a rigid type variable bound by a pattern with constructor SCons1 :: forall a (t :: [*]). a -> SList1 t -> SList1 (a : t), in an equation for ‘mapF1'’ at 1.lhs:72:13 ‘a’ is a rigid type variable bound by the type signature for mapF1' :: (a -> b) -> SList1 t -> SList1 (MapF' a b t) at 1.lhs:70:13 Relevant bindings include x :: a1 (bound at 1.lhs:72:20) f :: a -> b (bound at 1.lhs:72:10) mapF1' :: (a -> b) -> SList1 t -> SList1 (MapF' a b t) (bound at 1.lhs:71:3) In the first argument of ‘f’, namely ‘x’ In the first argument of ‘SCons1’, namely ‘(f x)’ And i noticed that `MapF'` type family does not enforce constraint on list element type: *Main> :t undefined :: SList1 (MapF' Int Char ('(:) Int '[])) undefined :: SList1 (MapF' Int Char ('(:) Int '[])) :: SList1 '[Char] but this should (shouldn't it?) be an error *Main> :t undefined :: SList1 (MapF' Float Char ('(:) Int '[])) undefined :: SList1 (MapF' Float Char ('(:) Int '[])) :: SList1 (MapF' Float Char '[Int]) only constraint on its kind: *Main> :t undefined :: SList1 (MapF' ('Just Int) Char ('(:) Int '[])) The third argument of ‘MapF'’ should have kind ‘[Maybe *]’, but ‘(:) Int '[]’ has kind ‘[*]’ In an expression type signature: SList1 (MapF' (Just Int) Char ((:) Int '[])) In the expression: undefined :: SList1 (MapF' (Just Int) Char ((:) Int '[])) Is there a way to restrict list element type to match the type of first MapF' type family's argument? And is there a way to write `map` on SList1?