Hi Paolino, There are some functions similar to that in HList (Data.HList.HArray). Check the repo http://code.haskell.org/HList for a version that uses more type families / gadts.
Maybe there is a way to take advantage of the fact that you've labelled the elements of the list, but extract isn't too bad if you don't: http://lpaste.net/94210. Regards, Adam On Sat, Oct 12, 2013 at 4:41 AM, Paolino <paolo.verone...@gmail.com> 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
