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