<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div>Yes, it's possible, but it's rather painful.</div><div><br></div><div>Here is my working attempt, written to be compatible with GHC 7.6.3. Better ones may be possible, but I'm doubtful.</div><div><br></div><div><div></div></div><blockquote type="cite"><div><div>{-# LANGUAGE TemplateHaskell, RankNTypes, TypeFamilies, TypeOperators,</div><div> DataKinds, ScopedTypeVariables, GADTs, PolyKinds #-}</div><div><br></div><div>module ListNat where</div><div><br></div><div>import Data.Singletons</div><div><br></div><div>$(singletons [d|</div><div> data Nat = Zero | Succ Nat deriving Eq</div><div> |])</div><div><br></div><div>-- in HEAD, these next two are defined in Data.Type.Equality</div><div>data a :~: b where</div><div> Refl :: a :~: a</div><div><br></div><div>gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r</div><div>gcastWith Refl x = x</div><div><br></div><div>-- functionality that subsumes this will be in the next release of singletons</div><div>reifyNatEq :: forall (m :: Nat) (n :: Nat). ((m :==: n) ~ True, SingI m, SingI n) => m :~: n</div><div>reifyNatEq =</div><div> case (sing :: Sing m, sing :: Sing n) of</div><div> (SZero, SZero) -> Refl</div><div> (SSucc (_ :: Sing m'), SSucc (_ :: Sing n')) -></div><div> gcastWith (reifyNatEq :: (m' :~: n')) Refl</div><div> _ -> bugInGHC -- this is necessary to prevent a spurious warning from GHC</div><div><br></div><div>data family X (n::Nat) :: * </div><div><br></div><div>data L (n::Nat) where </div><div> Q :: L (Succ n) -> X n -> L n </div><div> E :: L n</div><div><br></div><div>extract :: SingI n => L Zero -> X n</div><div>extract = aux</div><div> where</div><div> aux :: forall m n. (SingI m, SingI n) => L m -> X n</div><div> aux list =</div><div> case ((sing :: Sing m) %==% (sing :: Sing n), list) of</div><div> (_, E) -> error "Desired element does not exist"</div><div> (STrue, Q _ datum) -> gcastWith (reifyNatEq :: (m :~: n)) datum</div><div> (SFalse, Q rest _) -> aux rest</div><div><br></div><div>update :: forall n. SingI n => L Zero -> (X n -> X n) -> L Zero</div><div>update list upd = aux list</div><div> where</div><div> aux :: forall m. SingI m => L m -> L m</div><div> aux list =</div><div> case ((sing :: Sing m) %==% (sing :: Sing n), list) of</div><div> (_, E) -> error "Desired element does not exist"</div><div> (STrue, Q rest datum) -> gcastWith (reifyNatEq :: (m :~: n)) (Q rest (upd datum))</div><div> (SFalse, Q rest datum) -> Q (aux rest) datum</div></div><span></span></blockquote><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>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!</div><div><br></div><div>I hope this helps,</div><div>Richard</div><div><br></div><br><div><div>On Oct 12, 2013, at 4:41 AM, Paolino wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div dir="ltr"><div><div>Hello everyone,<br><br></div>I'm still trying to resolve my problem. I try to restate it in a simpler way.<br></div>Is it possible to write extract and update functions for L ?<br><div><br>import Data.Nat<br>
<br>data family X (n::Nat) :: * <br><br>data L (n::Nat) where <br> Q :: L (Succ n) -> X n -> L n <br> E :: L n<br><br>extract :: L Zero -> X n<br>extract = undefined<br><br>update :: L Zero -> (X n -> X n) -> L Zero<br>
update = undefined<br><br></div><div>Thanks for hints and help<br><br></div><div>paolino<br></div><div><br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">2013/10/7 Paolino <span dir="ltr"><<a href="mailto:paolo.veronelli@gmail.com" target="_blank">paolo.veronelli@gmail.com</a>></span><br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>Hello, I'm trying to use a type class to select an element from a list.<br></div><div>I would like to have a String "CC" as a value for l10'.<br>
</div><div><br></div><div><br>{-# LANGUAGE MultiParamTypeClasses, GADTs,FlexibleInstances, DataKinds ,TypeFamilies, KindSignatures, FlexibleContexts, OverlappingInstances, StandaloneDeriving, UndecidableInstances #-}<br>
<br><br><br>import Data.Nat<br>import Data.Monoid<br><br>data family X (n::Nat) :: * <br><br>data L (n::Nat) where <br> Q :: (Monoid (X n), Show (X n)) => L (Succ n) -> X n -> L n <br> E :: Monoid (X n) => L n<br>
<br>deriving instance Show (L n)<br>data instance X n = String String<br><br>instance Monoid (X n) where<br> String x `mappend` String y = String $ x `mappend` y<br> mempty = String ""<br>deriving instance Show (X n)<br>
<br>class Compose n n' where<br> compose :: L n -> L n -> X n'<br><br>instance Compose n n where<br> compose (Q _ x) (Q _ y) = x `mappend` y<br> compose _ _ = mempty<br><br>instance Compose n n' where<br>
compose (Q x _) (Q y _) = compose x y <br> compose _ _ = mempty<br><br>l0 :: L Zero<br>l0 = Q (Q E $ String "C") $ String "A" <br><br>l0' :: L Zero<br>l0' = Q (Q E $ String "C") $ String "B" <br>
<br><br>l10' :: X (Succ Zero)<br>l10' = compose l0 l0'<br><br>l00' :: X Zero<br>l00' = compose l0 l0'<br>{-<br><br>*Main> l00'<br>String "AB"<br>*Main> l10'<br>String ""<br>
<br>-}<br><br></div><div>Thanks for help.<span class="HOEnZb"><font color="#888888"><br><br></font></span></div><span class="HOEnZb"><font color="#888888"><div>paolino<br></div></font></span></div>
</blockquote></div><br></div>
_______________________________________________<br>Haskell-Cafe mailing list<br><a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>http://www.haskell.org/mailman/listinfo/haskell-cafe<br></blockquote></div><br></body></html>