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