[Haskell-cafe] Reinventing the wheel with HList.

[Nicholls, Mark]

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150624/0c63ba67/attachment.html>