Paolino | 7 Oct 17:36 2013
Picon

typeclass to select a list element

Hello, I'm trying to use a type class to select an element from a list.
I would like to have a String "CC" as a value for l10'.


{-# LANGUAGE MultiParamTypeClasses, GADTs,FlexibleInstances,  DataKinds ,TypeFamilies, KindSignatures, FlexibleContexts, OverlappingInstances, StandaloneDeriving, UndecidableInstances #-}



import Data.Nat
import Data.Monoid

data family X (n::Nat) :: *

data L (n::Nat) where   
    Q :: (Monoid (X n), Show (X n)) => L (Succ n) -> X n -> L n
    E :: Monoid (X n) => L n

deriving instance Show (L n)
data instance X n = String String

instance Monoid (X n) where
    String x `mappend` String y = String $ x `mappend` y
    mempty = String ""
deriving instance Show (X n)

class Compose n n' where
    compose :: L n  -> L n  -> X n'

instance Compose n n where
    compose (Q _ x) (Q _ y) = x `mappend` y
    compose _ _ = mempty

instance Compose n n' where
    compose (Q x _) (Q y _) = compose x y
    compose _ _ = mempty

l0 :: L Zero
l0 = Q (Q E $ String "C") $ String "A"

l0' :: L Zero
l0' = Q (Q E $ String "C") $ String "B"


l10' :: X (Succ Zero)
l10' = compose l0 l0'

l00' :: X Zero
l00' = compose l0 l0'
{-

*Main> l00'
String "AB"
*Main> l10'
String ""

-}

Thanks for help.

paolino
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Paolino | 12 Oct 10:41 2013
Picon

Re: typeclass to select a list element

Hello everyone,

I'm still trying to resolve my problem. I try to restate it in a simpler way.
Is it possible to write extract and update functions for L ?

import Data.Nat

data family X (n::Nat) :: *

data L (n::Nat) where   
    Q :: L (Succ n) -> X n -> L n
    E :: L n

extract :: L Zero -> X n
extract = undefined

update :: L Zero -> (X n -> X n) -> L Zero
update = undefined

Thanks for hints and help

paolino



2013/10/7 Paolino <paolo.veronelli <at> gmail.com>
Hello, I'm trying to use a type class to select an element from a list.
I would like to have a String "CC" as a value for l10'.


{-# LANGUAGE MultiParamTypeClasses, GADTs,FlexibleInstances,  DataKinds ,TypeFamilies, KindSignatures, FlexibleContexts, OverlappingInstances, StandaloneDeriving, UndecidableInstances #-}



import Data.Nat
import Data.Monoid

data family X (n::Nat) :: *

data L (n::Nat) where   
    Q :: (Monoid (X n), Show (X n)) => L (Succ n) -> X n -> L n
    E :: Monoid (X n) => L n

deriving instance Show (L n)
data instance X n = String String

instance Monoid (X n) where
    String x `mappend` String y = String $ x `mappend` y
    mempty = String ""
deriving instance Show (X n)

class Compose n n' where
    compose :: L n  -> L n  -> X n'

instance Compose n n where
    compose (Q _ x) (Q _ y) = x `mappend` y
    compose _ _ = mempty

instance Compose n n' where
    compose (Q x _) (Q y _) = compose x y
    compose _ _ = mempty

l0 :: L Zero
l0 = Q (Q E $ String "C") $ String "A"

l0' :: L Zero
l0' = Q (Q E $ String "C") $ String "B"


l10' :: X (Succ Zero)
l10' = compose l0 l0'

l00' :: X Zero
l00' = compose l0 l0'
{-

*Main> l00'
String "AB"
*Main> l10'
String ""

-}

Thanks for help.

paolino

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
adam vogt | 12 Oct 20:04 2013
Picon

Re: typeclass to select a list element

Hi Paolino,

There are some functions similar to that in HList (Data.HList.HArray).
Check the repo http://code.haskell.org/HList for a version that uses
more type families / gadts.

Maybe there is a way to take advantage of the fact that you've
labelled the elements of the list, but extract isn't too bad if you
don't: http://lpaste.net/94210.

Regards,
Adam

On Sat, Oct 12, 2013 at 4:41 AM, Paolino <paolo.veronelli <at> gmail.com> wrote:
> Hello everyone,
>
> I'm still trying to resolve my problem. I try to restate it in a simpler
> way.
> Is it possible to write extract and update functions for L ?
>
> import Data.Nat
>
>
> data family X (n::Nat) :: *
>
> data L (n::Nat) where
>     Q :: L (Succ n) -> X n -> L n
>     E :: L n
>
> extract :: L Zero -> X n
> extract = undefined
>
> update :: L Zero -> (X n -> X n) -> L Zero
> update = undefined
>
> Thanks for hints and help
>
> paolino
>
>
>
> 2013/10/7 Paolino <paolo.veronelli <at> gmail.com>
>>
>> Hello, I'm trying to use a type class to select an element from a list.
>> I would like to have a String "CC" as a value for l10'.
>>
>>
>> {-# LANGUAGE MultiParamTypeClasses, GADTs,FlexibleInstances,  DataKinds
>> ,TypeFamilies, KindSignatures, FlexibleContexts, OverlappingInstances,
>> StandaloneDeriving, UndecidableInstances #-}
>>
>>
>>
>> import Data.Nat
>> import Data.Monoid
>>
>> data family X (n::Nat) :: *
>>
>> data L (n::Nat) where
>>     Q :: (Monoid (X n), Show (X n)) => L (Succ n) -> X n -> L n
>>     E :: Monoid (X n) => L n
>>
>> deriving instance Show (L n)
>> data instance X n = String String
>>
>> instance Monoid (X n) where
>>     String x `mappend` String y = String $ x `mappend` y
>>     mempty = String ""
>> deriving instance Show (X n)
>>
>> class Compose n n' where
>>     compose :: L n  -> L n  -> X n'
>>
>> instance Compose n n where
>>     compose (Q _ x) (Q _ y) = x `mappend` y
>>     compose _ _ = mempty
>>
>> instance Compose n n' where
>>     compose (Q x _) (Q y _) = compose x y
>>     compose _ _ = mempty
>>
>> l0 :: L Zero
>> l0 = Q (Q E $ String "C") $ String "A"
>>
>> l0' :: L Zero
>> l0' = Q (Q E $ String "C") $ String "B"
>>
>>
>> l10' :: X (Succ Zero)
>> l10' = compose l0 l0'
>>
>> l00' :: X Zero
>> l00' = compose l0 l0'
>> {-
>>
>> *Main> l00'
>> String "AB"
>> *Main> l10'
>> String ""
>>
>> -}
>>
>> Thanks for help.
>>
>> paolino
>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
Richard Eisenberg | 13 Oct 04:47 2013

Re: typeclass to select a list element

Yes, it's possible, but it's rather painful.

Here is my working attempt, written to be compatible with GHC 7.6.3. Better ones may be possible, but I'm doubtful.

{-# LANGUAGE TemplateHaskell, RankNTypes, TypeFamilies, TypeOperators,
             DataKinds, ScopedTypeVariables, GADTs, PolyKinds #-}

module ListNat where

import Data.Singletons

$(singletons [d|
  data Nat = Zero | Succ Nat deriving Eq
  |])

-- in HEAD, these next two are defined in Data.Type.Equality
data a :~: b where
  Refl :: a :~: a

gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r
gcastWith Refl x = x

-- functionality that subsumes this will be in the next release of singletons
reifyNatEq :: forall (m :: Nat) (n :: Nat). ((m :==: n) ~ True, SingI m, SingI n) => m :~: n
reifyNatEq =
  case (sing :: Sing m, sing :: Sing n) of
    (SZero, SZero) -> Refl
    (SSucc (_ :: Sing m'), SSucc (_ :: Sing n')) ->
      gcastWith (reifyNatEq :: (m' :~: n')) Refl
    _ -> bugInGHC   -- this is necessary to prevent a spurious warning from GHC

data family X (n::Nat) :: * 

data L (n::Nat) where    
    Q :: L (Succ n) -> X n -> L n 
    E :: L n

extract :: SingI n => L Zero -> X n
extract = aux
  where
    aux :: forall m n. (SingI m, SingI n) => L m -> X n
    aux list =
      case ((sing :: Sing m) %==% (sing :: Sing n), list) of
        (_,      E)         -> error "Desired element does not exist"
        (STrue,  Q _ datum) -> gcastWith (reifyNatEq :: (m :~: n)) datum
        (SFalse, Q rest _)  -> aux rest

update :: forall n. SingI n => L Zero -> (X n -> X n) -> L Zero
update list upd = aux list
  where
    aux :: forall m. SingI m => L m -> L m
    aux list =
      case ((sing :: Sing m) %==% (sing :: Sing n), list) of
        (_, E) -> error "Desired element does not exist"
        (STrue, Q rest datum) -> gcastWith (reifyNatEq :: (m :~: n)) (Q rest (upd datum))
        (SFalse, Q rest datum) -> Q (aux rest) datum

Why is this so hard? There are two related sources of difficulty. The first is that `extract` and `update` require *runtime* information about the *type* parameter `n`. But, types are generally erased during compilation. So, the way to get the data you need is to use a typeclass (as your subject line suggests). The other source of difficulty is that you need to convince GHC that you've arrived at the right element when you get there; otherwise, your code won't type-check. The way to do this is, in my view, singletons.

For better or worse, your example requires checking the equality of numbers at a value other than Zero. The singletons library doesn't do a great job of this, which is why we need the very clunky reifyNatEq. I'm hoping to add better support for equality-oriented operations in the next release of singletons.

I'm happy to explain the details of the code above, but it might be better as Q&A instead of me just trying to walk through it -- there's a lot of gunk to stare at there!

I hope this helps,
Richard


On Oct 12, 2013, at 4:41 AM, Paolino wrote:

Hello everyone,

I'm still trying to resolve my problem. I try to restate it in a simpler way.
Is it possible to write extract and update functions for L ?

import Data.Nat

data family X (n::Nat) :: *

data L (n::Nat) where   
    Q :: L (Succ n) -> X n -> L n
    E :: L n

extract :: L Zero -> X n
extract = undefined

update :: L Zero -> (X n -> X n) -> L Zero
update = undefined

Thanks for hints and help

paolino



2013/10/7 Paolino <paolo.veronelli <at> gmail.com>
Hello, I'm trying to use a type class to select an element from a list.
I would like to have a String "CC" as a value for l10'.


{-# LANGUAGE MultiParamTypeClasses, GADTs,FlexibleInstances,  DataKinds ,TypeFamilies, KindSignatures, FlexibleContexts, OverlappingInstances, StandaloneDeriving, UndecidableInstances #-}



import Data.Nat
import Data.Monoid

data family X (n::Nat) :: *

data L (n::Nat) where   
    Q :: (Monoid (X n), Show (X n)) => L (Succ n) -> X n -> L n
    E :: Monoid (X n) => L n

deriving instance Show (L n)
data instance X n = String String

instance Monoid (X n) where
    String x `mappend` String y = String $ x `mappend` y
    mempty = String ""
deriving instance Show (X n)

class Compose n n' where
    compose :: L n  -> L n  -> X n'

instance Compose n n where
    compose (Q _ x) (Q _ y) = x `mappend` y
    compose _ _ = mempty

instance Compose n n' where
    compose (Q x _) (Q y _) = compose x y
    compose _ _ = mempty

l0 :: L Zero
l0 = Q (Q E $ String "C") $ String "A"

l0' :: L Zero
l0' = Q (Q E $ String "C") $ String "B"


l10' :: X (Succ Zero)
l10' = compose l0 l0'

l00' :: X Zero
l00' = compose l0 l0'
{-

*Main> l00'
String "AB"
*Main> l10'
String ""

-}

Thanks for help.

paolino

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Gmane