Re: [Haskell-cafe] typeclass to select a list element

[Paolino]

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.verone...@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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] typeclass to select a list element

[adam vogt]

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.verone...@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.verone...@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@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] typeclass to select a list element

[Richard Eisenberg]

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 
QA 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.verone...@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@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe