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