[Haskell-cafe] Reinventing the wheel with HList.
Adam Gundry
adam at well-typed.com
Wed Jun 24 15:31:59 UTC 2015
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/
More information about the Haskell-Cafe
mailing list