[Haskell-cafe] Reinventing the wheel with HList.

[Adam Gundry]

Hi,

The problem here is that, since `HList` is a data family, pattern
matching on a value of type `HList a` does not provide more information
about the variable `a`. It is only valid to pattern-match on `HNil` if
you already know that it has type `HList '[]`, hence the error message.

Instead, you probably want to use a GADT for singleton lists:

> data SList l where
>   Nil  :: SList '[]
>   Cons :: x -> SList xs -> SList (x ': xs)

Now it is possible for `add` to pattern-match on a constructor of
`SList` and refine the type.

(By the way, I don't think you need TMonoid'... just using TMonoid
should work.)

Hope this helps,

Adam


On 24/06/15 13:59, Nicholls, Mark wrote:
> My latest confusion….
> 
>  
> 
> I’ve got a typeclass (with associated types) monoid sort of thing….
> 
> I can get a Singleton family of Nat to be an instance of the typeclass.
> 
>  
> 
> Lists are sort of Natural numbers…with a bit of extra functionality…
> 
> So I should be able to take HList and make that a member of the same
> typeclass…
> 
>  
> 
> I fail for 2 reasons…1…I have to wrestle with the kinds…in a way I find
> ununderstandbly irritating.
> 
> And 2…because BOOM.
> 
> “is a rigid type variable bound by” blab la.
> 
>  
> 
> My Haskell in many ways is primitive…I seem to be messing with things
> beyond my ability….but that’s the way to learn I suppose.
> 
>  
> 
>> {-# LANGUAGE DataKinds #-}
> 
>> {-# LANGUAGE ExplicitForAll #-}
> 
>> {-# LANGUAGE FlexibleContexts #-}
> 
>> {-# LANGUAGE FlexibleInstances #-}
> 
>> {-# LANGUAGE GADTs #-}
> 
>> {-# LANGUAGE MultiParamTypeClasses #-}
> 
>> {-# LANGUAGE PolyKinds #-}
> 
>> {-# LANGUAGE StandaloneDeriving #-}
> 
>> {-# LANGUAGE TypeFamilies #-}
> 
>> {-# LANGUAGE TypeOperators #-}
> 
>> {-# LANGUAGE UndecidableInstances #-}
> 
>> {-# LANGUAGE ScopedTypeVariables #-}
> 
>  
> 
>> import Control.Effect
> 
>> import Control.Effect.Helpers.List
> 
>> import Control.Effect.WriteOnceWriter 
> 
>> import Prelude hiding ((>>=),(>>),return,fmap,fail)
> 
>> --import GHC.TypeLits
> 
>> import Data.Type.Equality
> 
>> import Data.Type.Bool
> 
>> --import Data.HList.HList
> 
>  
> 
>  
> 
>> data Nat where
> 
>>   Z :: Nat
> 
>>   S :: Nat -> Nat
> 
>  
> 
>> data family Sing (a :: k)
> 
>  
> 
>> data SNat (a :: Nat) where
> 
>>   SZ :: SNat 'Z
> 
>>   SS :: SNat a -> SNat ('S a)
> 
>  
> 
>> type family   (n :: Nat) :+ (m :: Nat) :: Nat
> 
>> type instance 'Z     :+ m = m
> 
>> type instance ('S n) :+ m = 'S (n :+ m)
> 
>  
> 
>  
> 
> Define something like a monoid over the types…
> 
> (note I have to wrestle with the kind signatures to get the instance of
> SNat to work, which is fine…but now closes doors to other instances)
> 
>  
> 
>> class TMonoid (m :: k -> *) where
> 
>>   type O m :: k
> 
>>   zero :: m (O m)
> 
>>   type TPlus m (d :: k) (e :: k) :: k
> 
>>   add :: m a -> m b -> m (TPlus m a b)
> 
>  
> 
> And this works quite nicely
> 
>  
> 
>> instance TMonoid SNat where
> 
>>   type O SNat = 'Z
> 
>>   zero = SZ
> 
>>   type TPlus SNat a b = a :+ b
> 
>>   add SZ b = b
> 
>>   add (SS a) b = SS (add a b)
> 
>  
> 
> Now….
> 
>  
> 
> (I have to declare different kind?....I can’t get a single simple
> declaration of TMonoid?)
> 
>  
> 
>> class TMonoid' (m :: [*] -> *) where
> 
>>   type O' m :: [*]
> 
>>   zero' :: m (O' m)
> 
>>   type TPlus' m (d :: [*]) (e :: [*]) :: [*]
> 
>>   add' :: m a -> m b -> m (TPlus' m a b)
> 
>  
> 
> Steal the definition of HList
> 
>  
> 
>> data family HList (l::[*]) :: *
> 
>  
> 
>> data instance HList '[] = HNil
> 
>> data instance HList (x ': xs) = x `HCons` HList xs
> 
>  
> 
> And try to construct an analogous TMonoid of it…
> 
>  
> 
>> instance TMonoid' HList where
> 
>>   type O' HList = '[]
> 
>>   zero' = HNil
> 
>>   type TPlus' HList a b = a :++ b
> 
>>   add' HNil b = b
> 
>>   add' (HCons x xs) ys = HCons x (add' xs ys)
> 
>  
> 
> BOOM
> 
>  
> 
> Couldn't match type ‘a’ with ‘'[]’
> 
>       ‘a’ is a rigid type variable bound by
> 
>           the type signature for
> 
>             add' :: HList a -> HList b -> HList (TPlus' HList a b)
> 
>           at broadcast2.lhs:90:5
> 
>     Expected type: HList a
> 
>       Actual type: HList '[]
> 
>     Relevant bindings include
> 
>       add' :: HList a -> HList b -> HList (TPlus' HList a b)
> 
>         (bound at broadcast2.lhs:90:5)
> 
>     In the pattern: HNil
> 
>     In an equation for ‘add'’: add' HNil b = b
> 
>     In the instance declaration for ‘TMonoid' HList’
> 
>  
> 
> Hmmm….confused…why does
> 
>  
> 
> add SZ b = b
> 
>  
> 
> work, but the analogous
> 
>  
> 
> add' HNil b = b
> 
>  
> 
> fail


-- 
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/