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.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
