Reinventing the wheel with HList.
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 CONFIDENTIALITY NOTICE This e-mail (and any attached files) is confidential and protected by copyright (and other intellectual property rights). If you are not the intended recipient please e-mail the sender and then delete the email and any attached files immediately. Any further use or dissemination is prohibited. While MTV Networks Europe has taken steps to ensure that this email and any attachments are virus free, it is your responsibility to ensure that this message and any attachments are virus free and do not affect your systems / data. Communicating by email is not 100% secure and carries risks such as delay, data corruption, non-delivery, wrongful interception and unauthorised amendment. If you communicate with us by e-mail, you acknowledge and assume these risks, and you agree to take appropriate measures to minimise these risks when e-mailing us. MTV Networks International, MTV Networks UK & Ireland, Greenhouse, Nickelodeon Viacom Consumer Products, VBSi, Viacom Brand Solutions International, Be Viacom, Viacom International Media Networks and VIMN and Comedy Central are all trading names of MTV Networks Europe. MTV Networks Europe is a partnership between MTV Networks Europe Inc. and Viacom Networks Europe Inc. Address for service in Great Britain is 17-29 Hawley Crescent, London, NW1 8TT.
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/
Brilliant....let me have a go...half the problem here is there seems to be about 5 different ways to do the same thing...all slightly different...and all with creases in it....I'm probably more at home with GADTs anyway.
-----Original Message----- From: Haskell-Cafe [mailto:haskell-cafe-bounces@haskell.org] On Behalf Of Adam Gundry Sent: 24 June 2015 4:32 PM To: haskell-cafe@haskell.org Subject: Re: [Haskell-cafe] Reinventing the wheel with HList.
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/ _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe CONFIDENTIALITY NOTICE
This e-mail (and any attached files) is confidential and protected by copyright (and other intellectual property rights). If you are not the intended recipient please e-mail the sender and then delete the email and any attached files immediately. Any further use or dissemination is prohibited. While MTV Networks Europe has taken steps to ensure that this email and any attachments are virus free, it is your responsibility to ensure that this message and any attachments are virus free and do not affect your systems / data. Communicating by email is not 100% secure and carries risks such as delay, data corruption, non-delivery, wrongful interception and unauthorised amendment. If you communicate with us by e-mail, you acknowledge and assume these risks, and you agree to take appropriate measures to minimise these risks when e-mailing us. MTV Networks International, MTV Networks UK & Ireland, Greenhouse, Nickelodeon Viacom Consumer Products, VBSi, Viacom Brand Solutions International, Be Viacom, Viacom International Media Networks and VIMN and Comedy Central are all trading names of MTV Networks Europe. MTV Networks Europe is a partnership between MTV Networks Europe Inc. and Viacom Networks Europe Inc. Address for service in Great Britain is 17-29 Hawley Crescent, London, NW1 8TT.
participants (2)
-
Adam Gundry -
Nicholls, Mark