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/