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