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