[Haskell-beginners] Type constraints of type family arguments

[Dmitriy Matrosov]

> {-# 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?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/beginners/attachments/20160330/782d22cd/attachment.html>