[Haskell-cafe] Reinventing the wheel with HList.

Nicholls, Mark nicholls.mark at vimn.com
Wed Jun 24 15:37:21 UTC 2015


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 at haskell.org] On Behalf Of
>Adam Gundry
>Sent: 24 June 2015 4:32 PM
>To: haskell-cafe at 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 at 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.



More information about the Haskell-Cafe mailing list