packages feed

HList (empty) → 0.1

raw patch · 22 files changed

+3142/−0 lines, 22 filesdep +basesetup-changed

Dependencies added: base

Files

+ Data/HList.hs view
@@ -0,0 +1,60 @@+{-# LANGUAGE MagicHash #-}+{-+OOHaskell (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke++This module gathers the API that we need for OOP in Haskell.  We+basically select a certain configuration of the HList library, and we+also import modules that are needed for mutable data and monads. Note+on overlapping: Needed for the chosen model of labels. Other models+can be used instead, but the chosen look better in types.+-}+++module Data.HList (++ module Data.HList.CommonMain,+ module Data.HList.GhcSyntax,+ module Data.HList.GhcRecord,+ module Data.HList.GhcExperiments,+ module Data.STRef,+ module Data.IORef,+ module Data.Typeable,+ module Control.Monad,+ module Control.Monad.ST,+ module Control.Monad.Fix,+ module GHC.IOBase,+-- module DeepNarrow,+-- module Nominal,+-- module New,+-- module Data.HList.HList+ concrete,+ (#)+) where+++import Data.HList.CommonMain hiding ( HDeleteMany+                         , hDeleteMany+                         , TypeCast+                         , typeCast+                         )++import Data.HList.GhcSyntax+import Data.HList.GhcRecord+import Data.HList.GhcExperiments++import Data.STRef+import Data.IORef+import Data.Typeable+import Control.Monad+import Control.Monad.ST+import Control.Monad.Fix+import GHC.IOBase hiding (stToIO, writeIORef, readIORef, newIORef, IORef,unsafeIOToST,unsafeSTToIO)++infixr 9 #+(#) :: (HasField l r v) => r -> l -> v+m # field = (m .!. field)++concrete :: (MonadFix m) => (a -> m a) -> a -> m a+concrete generator self = generator self+ where+  _ = mfix generator
+ Data/HList/CommonMain.hs view
@@ -0,0 +1,36 @@+{-++   The HList library++   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke++   This is a next-to-main module that loads all modules that at least+   *compile* fine for all the models of interest. See the Makefile+   for ways to run different models.++-}++module Data.HList.CommonMain (++   module Data.HList.FakePrelude+ , module Data.HList.HListPrelude+ , module Data.HList.HArray+ , module Data.HList.HOccurs+ , module Data.HList.HTypeIndexed+ , module Data.HList.TIP+ , module Data.HList.TIC+ , module Data.HList.HZip+ , module Data.HList.Record+ , module Data.HList.Variant+) where++import Data.HList.FakePrelude+import Data.HList.HListPrelude+import Data.HList.HArray+import Data.HList.HOccurs+import Data.HList.HTypeIndexed+import Data.HList.TIP+import Data.HList.TIC+import Data.HList.HZip+import Data.HList.Record+import Data.HList.Variant
+ Data/HList/FakePrelude.hs view
@@ -0,0 +1,256 @@+{-# LANGUAGE EmptyDataDecls, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances #-}++{-+   The HList library++   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke++   Some very basic technology for faking dependent types in Haskell.+-}++module Data.HList.FakePrelude where+++{-----------------------------------------------------------------------------}++-- Type-level Booleans++data HTrue; hTrue :: HTrue; hTrue = undefined+data HFalse; hFalse :: HFalse; hFalse = undefined+class HBool x; instance HBool HTrue; instance HBool HFalse+instance Show HTrue where show _ = "HTrue"+instance Show HFalse where show _ = "HFalse"+++-- Conjunction of type-level Booleans++class (HBool t, HBool t', HBool t'') => HAnd t t' t'' | t t' -> t''+ where+  hAnd :: t -> t' -> t''++instance HAnd HFalse HFalse HFalse+ where+  hAnd _ _ = hFalse++instance HAnd HTrue HFalse HFalse+ where+  hAnd _ _ = hFalse++instance HAnd HFalse HTrue HFalse+ where+  hAnd _ _ = hFalse++instance HAnd HTrue HTrue HTrue+ where+  hAnd _ _ = hTrue+++-- Disjunction of type-level Booleans++class (HBool t, HBool t', HBool t'') => HOr t t' t'' | t t' -> t''+ where+  hOr :: t -> t' -> t''++instance HOr HFalse HFalse HFalse+ where+  hOr _ _ = hFalse++instance HOr HTrue HFalse HTrue+ where+  hOr _ _ = hTrue++instance HOr HFalse HTrue HTrue+ where+  hOr _ _ = hTrue++instance HOr HTrue HTrue HTrue+ where+  hOr _ _ = hTrue+++-- Type-level conditional++class HBool t => HCond t x y z | t x y -> z+ where+  hCond :: t -> x -> y -> z++instance HCond HFalse x y y+ where+  hCond _ _ y = y++instance HCond HTrue x y x+ where+  hCond _ x _ = x+++-- We could define all kinds of further Boolean operations.+-- We omit everything what's not needed for the code in the paper.+++{-----------------------------------------------------------------------------}++-- Type-level naturals++data HZero+data HSucc n++hZero :: HZero; hZero = undefined+hSucc :: HNat n => n -> HSucc n; hSucc _ = undefined+hPred :: HNat n => HSucc n -> n; hPred _ = undefined++class HNat n+instance HNat HZero+instance HNat n => HNat (HSucc n)++instance Show HZero where show _ = "HZero"+instance Show (HSucc HZero)+ where show _ = "HSucc HZero"+instance (HNat n, Show (HSucc n)) => Show (HSucc (HSucc n))+ where show n = "HSucc (" ++ show (hPred n) ++ ")"++class HNat n => HNat2Integral n+ where+  hNat2Integral :: Integral i => n -> i++instance HNat2Integral HZero+ where+  hNat2Integral _ = 0++instance HNat2Integral n => HNat2Integral (HSucc n)+ where+  hNat2Integral n = hNat2Integral (hPred n) + 1+++{-----------------------------------------------------------------------------}++-- Type-level maybies++data HNothing  = HNothing  deriving Show+data HJust x   = HJust x   deriving Show+++{-----------------------------------------------------------------------------}++-- Equality for types++class HBool b => HEq x y b | x y -> b+++-- Equality instances for naturals++instance HEq HZero HZero HTrue+instance HNat n => HEq HZero (HSucc n) HFalse+instance HNat n => HEq (HSucc n) HZero HFalse+instance (HNat n, HNat n', HEq  n n' b )+      =>  HEq (HSucc n) (HSucc n') b++hEq :: HEq x y b => x -> y -> b+hEq =  undefined+++{-----------------------------------------------------------------------------}++-- Staged equality+--  - Establish type equality statically+--  - Establish remaining value-level equality dynamically++class HStagedEq x y+ where+  hStagedEq :: x -> y -> Bool+++{-----------------------------------------------------------------------------}++-- Less than++class HBool b => HLt x y b | x y -> b+++-- Equality instances for naturals++instance HLt HZero HZero HFalse+instance HNat n => HLt HZero (HSucc n) HTrue+instance HNat n => HLt (HSucc n) HZero HFalse+instance (HNat n, HNat n', HLt  n n' b)+      =>  HLt (HSucc n) (HSucc n') b++hLt   :: HLt x y b => x -> y -> b+hLt _ =  undefined+++{-----------------------------------------------------------------------------}++-- A predicate for type equality+-- There are different implementations.+-- See imports in Main*.hs++class HBool b => TypeEq x y b | x y -> b+++-- Rely on lazy show for type-level Booleans+typeEq :: TypeEq t t' b => t -> t' -> b+typeEq = undefined+++-- A more disciplined version: based on proxies+proxyEq :: TypeEq t t' b => Proxy t -> Proxy t' -> b+proxyEq _ _ = undefined+++{-----------------------------------------------------------------------------}++-- Type-safe cast++class TypeCast x y | x -> y, y -> x+ where+  typeCast :: x -> y+++{-----------------------------------------------------------------------------}++-- A phantom type for type proxies++data Proxy e+instance Show (Proxy e) where show _ = "Proxy"++proxy :: Proxy e+proxy =  undefined++toProxy :: e -> Proxy e+toProxy _ = undefined++unProxy :: Proxy e -> e+unProxy =  undefined+++{-----------------------------------------------------------------------------}++-- Type equality and disequality++class TypeEqTrue x y+class TypeEqFalse x y++typeEqTrue :: TypeEqTrue x y => x -> y -> ()+typeEqTrue _ _ = ()++typeEqFalse :: TypeEqFalse x y => x -> y -> ()+typeEqFalse _ _ = ()+++{-----------------------------------------------------------------------------}++-- Subtyping++class SubType l l'++subType :: SubType l l' => l -> l' -> ()+subType _ _ = ()+++{-----------------------------------------------------------------------------}++-- A class without instances for explicit failure+class Fail x+++{-----------------------------------------------------------------------------}
+ Data/HList/GhcExperiments.hs view
@@ -0,0 +1,67 @@+{-# LANGUAGE KindSignatures,MultiParamTypeClasses,FunctionalDependencies,FlexibleInstances, FlexibleContexts, UndecidableInstances #-}++{-+   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke++   This module gathers experiments that do not work with Hugs.+-}++module Data.HList.GhcExperiments where++import Data.HList.FakePrelude+import Data.HList.HListPrelude++class HDeleteMany e l l' | e l -> l'+ where+  hDeleteMany :: Proxy e -> l -> l'++instance HDeleteMany e HNil HNil+ where+  hDeleteMany _ HNil = HNil++instance (HList l, HDeleteMany e l l')+      => HDeleteMany e (HCons e l) l'+ where+  hDeleteMany p (HCons _ l) = hDeleteMany p l++{-++-- Hopelessly overlapping++instance (HList l, HDeleteMany e l l')+      => HDeleteMany e (HCons e' l) (HCons e' l')+ where+  hDeleteMany p (HCons e' l)+   =+     HCons e' (hDeleteMany p l)++-}++instance ( HList l+         , HDeleteMany e l l'+         , TypeCast (HCons e' l') l''+         )+      =>   HDeleteMany e (HCons e' l) l''+ where+  hDeleteMany p (HCons e' l)+   =+     typeCast (HCons e' (hDeleteMany p l))+++-----------------------------------------------------------------------------++-- Test for type constructors++-- signature: * -> *+class IsTC1 x (f :: * -> *) b | x f -> b+instance TypeCast HTrue b => IsTC1 (f a) f b+instance TypeCast HFalse b => IsTC1 f x b++-- signature: * -> * -> *+class IsTC2 x (f :: * -> * -> *) b | x f -> b+instance TypeCast HTrue b => IsTC2 (f a b) f b+instance TypeCast HFalse b => IsTC2 f x b++-- Sample+funType :: IsTC2 t (->) b => t -> b+funType = undefined
+ Data/HList/GhcRecord.hs view
@@ -0,0 +1,288 @@+{-# LANGUAGE PatternSignatures, ScopedTypeVariables, EmptyDataDecls,+  FunctionalDependencies, FlexibleInstances, FlexibleContexts,+  MultiParamTypeClasses, UndecidableInstances #-}++{-+   The HList library++   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke++   Extensible records -- operations that (may) require GHC++   See Record.hs for the base module.+-}++module Data.HList.GhcRecord where++import Data.HList.FakePrelude+import Data.HList.HListPrelude+import Data.HList.HArray+import Data.HList.Record+import Data.Typeable+++{-----------------------------------------------------------------------------}++-- A variation on update.+-- Replace a proxy by a value of the proxied type.+hUnproxyLabel :: (HUpdateAtHNat n (LVPair l a) t l', HFind l ls n,+                               RecordLabels t ls,+                               HasField l t (Proxy a)) =>+                                             l -> a -> Record t -> Record l'+hUnproxyLabel l v r = hUpdateAtLabel l v r+ where+  tpe :: a -> Proxy a -> ()+  tpe _ _ = ()+  _ = tpe v (hLookupByLabel l r)+++{-----------------------------------------------------------------------------}++-- Test for values; refuse proxies++hasNoProxies :: HasNoProxies r+             => Record r -> ()+hasNoProxies = const ()+++data ProxyFound x+class HasNoProxies l+instance HasNoProxies HNil+instance Fail (ProxyFound x) => HasNoProxies (HCons (Proxy x) l)+instance Fail (ProxyFound x) => HasNoProxies (HCons (LVPair lab (Proxy x)) l)+instance HasNoProxies l => HasNoProxies (HCons e l)+++{-----------------------------------------------------------------------------}++-- Narrow a record to a different record type++-- First is the `monadic' version, which returns the `failure indictator'+-- (HNothing) if the narrowing fails because the source does not have+-- all the fields for the target.+class  NarrowM a b res | a b -> res where+    narrowM :: Record a -> Record b -> res++instance NarrowM a HNil (HJust (Record HNil)) where+    narrowM _ _ = HJust emptyRecord++instance (H2ProjectByLabels (HCons l HNil) a rin rout,+          NarrowM' rin rout b res)+    => NarrowM a (HCons (LVPair l v) b) res where+    narrowM (Record a) _ = narrowM' rin rout (undefined::b)+     where+        (rin,rout) = h2projectByLabels (undefined::(HCons l HNil)) a++class  NarrowM' rin rout b res | rin rout b -> res where+    narrowM' :: rin -> rout -> b -> res++instance NarrowM' HNil rout b HNothing where+    narrowM' _ _ _ = HNothing++instance (NarrowM rout b res',+          NarrowM'' f res' res)+    => NarrowM' (HCons f HNil) rout b res where+    narrowM' (HCons f HNil) rout b =+        narrowM'' f (narrowM (Record rout) (Record b))++class  NarrowM'' f r r' | f r -> r' where+    narrowM'' :: f -> r -> r'++instance NarrowM'' f HNothing HNothing where+    narrowM'' _ _ = HNothing++instance NarrowM'' f (HJust (Record r)) (HJust (Record (HCons f r))) where+    narrowM'' f (HJust (Record r)) = HJust (Record (HCons f r))+++class  Narrow a b+ where narrow :: Record a -> Record b++instance Narrow a HNil+ where   narrow _ = emptyRecord++instance ( Narrow rout r'+         , H2ProjectByLabels (HCons l HNil) r (HCons (LVPair l v) HNil) rout+         ) => Narrow r (HCons (LVPair l v) r')+  where+    narrow (Record r) = Record (HCons f r')+      where+        (HCons f HNil,rout) = h2projectByLabels (undefined::(HCons l HNil)) r+        (Record r')    = narrow (Record rout)+++{-----------------------------------------------------------------------------}++-- Narrow two records to their least-upper bound++class LubNarrow a b c | a b -> c+ where+  lubNarrow :: a -> b -> (c,c)++instance ( RecordLabels a la+         , RecordLabels b lb+         , HTIntersect la lb lc+         , H2ProjectByLabels lc a c aout+         , H2ProjectByLabels lc b c bout+         , HRLabelSet c+         )+      => LubNarrow (Record a) (Record b) (Record c)+ where+  lubNarrow ra@(Record _) rb@(Record _) =+     ( hProjectByLabels (undefined::lc) ra+     , hProjectByLabels (undefined::lc) rb+     )+++{-----------------------------------------------------------------------------}++-- List constructors that also LUB together++data NilLub+nilLub :: NilLub+nilLub = undefined :: NilLub++class ConsLub h t l | h t -> l+ where+  consLub :: h -> t -> l++instance ConsLub e  NilLub [e]+ where+  consLub h _ = [h]++instance LubNarrow e0 e1 e2 => ConsLub e0 [e1] [e2]+ where+  consLub h t = fst (head z) : map snd (tail z)+   where+    z = map (lubNarrow h) (undefined:t)+++{-----------------------------------------------------------------------------}++-- Extension of lubNarrow to a heterogeneous list++class HLub l e | l -> e+ where+  hLub :: l -> [e]++instance ( LubNarrow h h' e+         )+      => HLub (HCons h (HCons h' HNil)) e+ where+  hLub (HCons h (HCons h' _)) = [fst ee, snd ee]+   where+    ee = lubNarrow h h'++instance ( HLub (HCons h (HCons h'' t)) e'+         , HLub (HCons h' (HCons h'' t)) e''+         , LubNarrow e' e'' e+         , HLub (HCons e (HCons h'' t)) e+         )+      => HLub (HCons h (HCons h' (HCons h'' t))) e+ where+  hLub (HCons h (HCons h' t)) = fst e : ( snd e : tail r )+   where+    e' = hLub (HCons h t)+    e'' = hLub (HCons h' t)+    e = lubNarrow (head e') (head e'')+    r = hLub (HCons (fst e) t)++++{-----------------------------------------------------------------------------}+-- Record equivalence modulo field order+-- Decide if two records r1 and r2 are identical or differ only in the order+-- of their fields.+-- If the two record types are indeed equivalent, return the witness of+-- their equivalence, (HJust (r1->r2,r2->r1)). If they are not equivalent,+-- return HNothing+-- The function equivR does not examine the values of its arguments:+-- it needs only their types.++-- The algorithm is simple: two records are equivalent if one can be narrowed+-- to the other, and vice versa. The narrowing coercions are the desired+-- witnesses.+-- The obvious optimization is to check first if two records are of the same+-- type. That requires TypeEq however. Perhaps we shouldn't use it here.+-- Use of the record narrowing tacitly assumes that the label of a record+-- field uniquely determines the type of the field value. Therefore, we+-- should not use equivR on two records with inconsistent labeling...++class RecordEquiv r1 r2 res | r1 r2 -> res where+    equivR :: Record r1 -> Record r2 -> res+++{-+instance (TypeEq r1 r2 b, RecordEquiv' b r1 r2 res)+    => RecordEquiv r1 r2 res where+    equivR _ _ = equivR' (undefined::b) (undefined::r1) (undefined::r2)+-- Two records have the same type: the fast path+instance RecordEquiv' HTrue r r+                      (HJust (Record r->Record r,Record r->Record r)) where+    equivR' _ _ _ = HJust (id,id)+-}++instance (NarrowM r1 r2 r12, NarrowM r2 r1 r21,+          RecordEquiv' (Record r1->r12) (Record r2->r21) res)+    => RecordEquiv r1 r2 res where+    equivR r1 r2 = equivR' r1p r2p+     where r1p (r1 :: Record r1) = narrowM r1 r2+           r2p (r2 :: Record r2) = narrowM r2 r1++class RecordEquiv' pj1 pj2 res | pj1 pj2 -> res where+    equivR' :: pj1 -> pj2 -> res++instance RecordEquiv' (r1->HJust r2) (r2->HJust r1) (HJust (r1->r2,r2->r1))+    where+    equivR' r12 r21 = HJust (unj.r12,unj.r21)+     where unj (HJust x) = x++-- r2 has something that r1 doesn't+instance RecordEquiv' (r1->HNothing) pj2 HNothing where+    equivR' _ _ = HNothing++-- r1 is a strict superset of r2+instance RecordEquiv' (r1->HJust r2) (r2->HNothing) HNothing where+    equivR' _ _ = HNothing+++{-----------------------------------------------------------------------------}+-- Typeable instances++hNilTcName :: TyCon+hNilTcName = mkTyCon "HList.HNil"+instance Typeable HNil+ where+  typeOf _ = mkTyConApp hNilTcName []++hConsTcName :: TyCon+hConsTcName = mkTyCon "HList.HCons"+instance (Typeable x, Typeable y) => Typeable (HCons x y)+ where+  typeOf (HCons x y)+   = mkTyConApp hConsTcName [ typeOf x, typeOf y ]++recordTcName :: TyCon+recordTcName = mkTyCon "HList.Record"+instance Typeable x => Typeable (Record x)+ where+  typeOf (Record x)+   = mkTyConApp recordTcName [ typeOf x ]++hFieldTcName :: TyCon+hFieldTcName = mkTyCon "HList.F"+instance (Typeable x, Typeable y) => Typeable (LVPair x y)+ where+  typeOf _+   = mkTyConApp hFieldTcName [ typeOf (undefined::x), typeOf (undefined::y)  ]++proxyTcName :: TyCon+proxyTcName = mkTyCon "HList.Proxy"+instance Typeable x => Typeable (Proxy x)+ where+  typeOf (_::Proxy x)+   = mkTyConApp proxyTcName [ typeOf (undefined::x) ]+++{-----------------------------------------------------------------------------}+
+ Data/HList/GhcSyntax.hs view
@@ -0,0 +1,97 @@+{-# LANGUAGE FlexibleContexts #-}+{-+   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke++   Some dedicated infix operators at the type and the value level.+-}++module Data.HList.GhcSyntax where++import Data.HList.HArray (HUpdateAtHNat())+import Data.HList.FakePrelude+import Data.HList.HListPrelude+import Data.HList.HOccurs+import Data.HList.Record+import Data.HList.GhcRecord+import Data.HList.TIP+import Data.HList.TIC+++{-----------------------------------------------------------------------------}++-- Convenience notation for type sequences++infixr 2 :*:+infixr 2 .*.++type e :*: l = HCons e l++(.*.) :: HExtend e l l' => e -> l -> l'+(.*.) =  hExtend+++{-----------------------------------------------------------------------------}++-- Convenience notation for records++infixr 4 :=:+type l :=: v = LVPair l v++infixr 4 .=.+(.=.) :: l -> v -> LVPair l v+l .=. v = newLVPair l v++infixr 3 .!.+(.!.) :: (HasField l r v) => r -> l -> v+r .!. l =  hLookupByLabel l r++infixl 1 .-.+(.-.) :: (H2ProjectByLabels (HCons e HNil) t t1 t2) => Record t -> e -> Record t2+r .-. l =  hDeleteAtLabel l r++infixl 1 .@.+(.@.) :: (HUpdateAtHNat n (LVPair t t1) t2 l',+         HFind t ls n,+         RecordLabels t2 ls) =>+        Record t2 -> LVPair t t1 -> Record l'+r .@. f@(LVPair v) =  hUpdateAtLabel (labelLVPair f) v r++infixr 1 .^.+(.^.) :: (HasField t t2 (Proxy t1),+         RecordLabels t2 ls,+         HFind t ls n,+         Data.HList.HArray.HUpdateAtHNat n (LVPair t t1) t2 l') =>+         LVPair t t1 -> Record t2 -> Record l'+f@(LVPair v) .^. r = hUnproxyLabel (labelLVPair f) v r++infixr 1 .<.+(.<.) :: (HasField t t2 t1,+         RecordLabels t2 ls,+         HFind t ls n,+         HUpdateAtHNat n (LVPair t t1) t2 l') =>+        LVPair t t1 -> Record t2 -> Record l'+f@(LVPair v) .<. r = hTPupdateAtLabel (labelLVPair f) v r++infixl 1 .<++.+(.<++.) :: (HLeftUnion r r' r'') => r -> r' -> r''+r .<++. r' = hLeftUnion r r'+++{-----------------------------------------------------------------------------}++-- Convenience notation for TIRs++infixr 2 :+:+infixr 2 .+.++type e :+: l = HCons (Proxy e) l++(.+.) :: ( HTypeIndexed l+         , HTypeProxied l+         , HOccursNot (Proxy e) l+         )+      => e -> TIP l -> TIP (HCons (Proxy e) l)+e .+. r = hExtend (toProxy e) r+++{-----------------------------------------------------------------------------}
+ Data/HList/HArray.hs view
@@ -0,0 +1,249 @@+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances,+  FlexibleContexts, UndecidableInstances #-}+{-+   The HList library++   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke++   Array-like access to HLists.+ -}++module Data.HList.HArray where++import Data.HList.FakePrelude+import Data.HList.HListPrelude+++{-----------------------------------------------------------------------------}++-- A lookup operation++class HNat n => HLookupByHNat n l e | n l -> e+ where+  hLookupByHNat :: n -> l -> e++instance HLookupByHNat HZero (HCons e l) e+ where+  hLookupByHNat _ (HCons e _) = e++instance (HLookupByHNat n l e', HNat n)+      => HLookupByHNat (HSucc n) (HCons e l) e'+ where+  hLookupByHNat n (HCons _ l) = hLookupByHNat (hPred n) l+++{-----------------------------------------------------------------------------}++-- A delete operation++class HNat n => HDeleteAtHNat n l l' | n l -> l'+ where+  hDeleteAtHNat :: n -> l -> l'++instance HDeleteAtHNat HZero (HCons e l) l+ where+  hDeleteAtHNat _ (HCons _ l) = l++instance (HDeleteAtHNat n l l', HNat n)+      => HDeleteAtHNat (HSucc n) (HCons e l) (HCons e l')+ where+  hDeleteAtHNat n (HCons e l) = HCons e (hDeleteAtHNat (hPred n) l)+++{-----------------------------------------------------------------------------}++-- An update operation++class HNat n => HUpdateAtHNat n e l l' | n e l -> l', l' n -> e+ where+  hUpdateAtHNat :: n -> e -> l -> l'++instance HUpdateAtHNat HZero e' (HCons e l) (HCons e' l)+ where+  hUpdateAtHNat _ e' (HCons _ l) = HCons e' l++instance (HUpdateAtHNat n e' l l', HNat n)+      => HUpdateAtHNat (HSucc n) e' (HCons e l) (HCons e l')+ where+  hUpdateAtHNat n e' (HCons e l)+   = HCons e (hUpdateAtHNat (hPred n) e' l)+++{-----------------------------------------------------------------------------}++-- Splitting an array according to indices+hSplitByHNats :: (HSplitByHNats' ns l' l'1 l'', HMap (HAddTag HTrue) l l') =>+                ns -> l -> (l'1, l'')+hSplitByHNats ns l = hSplitByHNats' ns (hFlag l)++class HNats ns => HSplitByHNats' ns l l' l'' | ns l -> l' l''+ where+  hSplitByHNats' :: ns -> l -> (l',l'')++instance HSplit l l' l''+      => HSplitByHNats' HNil l HNil l'+ where+  hSplitByHNats' HNil l = (HNil,l')+   where+    (l',_) = hSplit l++instance ( HLookupByHNat n l (e,b)+         , HUpdateAtHNat n (e,HFalse) l l'''+         , HSplitByHNats' ns l''' l' l''+         )+      =>   HSplitByHNats' (HCons n ns) l (HCons e l') l''+ where+  hSplitByHNats' (HCons n ns) l = (HCons e l',l'')+   where+    (e,_)    = hLookupByHNat  n l+    l'''     = hUpdateAtHNat  n (e,hFalse) l+    (l',l'') = hSplitByHNats' ns l'''+++{-----------------------------------------------------------------------------}++-- Another projection operation++class HNats ns => HProjectByHNats ns l l' | ns l -> l'+ where+  hProjectByHNats :: ns -> l -> l'++instance HProjectByHNats HNil HNil HNil+ where+  hProjectByHNats _ _ = HNil++instance HProjectByHNats HNil (HCons e l) HNil+ where+  hProjectByHNats _ _ = HNil++instance ( HLookupByHNat n (HCons e l) e'+         , HProjectByHNats ns (HCons e l) l'+         )+         => HProjectByHNats (HCons n ns) (HCons e l) (HCons e' l')+ where+  hProjectByHNats (HCons n ns) l = HCons e' l'+   where e' = hLookupByHNat n l+         l' = hProjectByHNats ns l+++{-----------------------------------------------------------------------------}++-- The complement of projection++class HProjectAwayByHNats ns l l' | ns l -> l'+ where+  hProjectAwayByHNats :: ns -> l -> l'++instance ( HLength l len+         , HBetween len nats+         , HDiff nats ns ns'+         , HProjectByHNats ns' l l'+         )+           => HProjectAwayByHNats ns l l'+ where+  hProjectAwayByHNats ns l = l'+   where+    len  = hLength l+    nats = hBetween len+    ns'  = hDiff nats ns+    l'   = hProjectByHNats ns' l+++{-----------------------------------------------------------------------------}++-- Generate naturals from 1 to x - 1++class HBetween x y | x -> y+ where+  hBetween :: x -> y++instance HBetween (HSucc HZero) (HCons HZero HNil)+ where+  hBetween _ = HCons hZero HNil++instance ( HNat x+         , HBetween (HSucc x) y+         , HAppend y (HCons (HSucc x) HNil) z+         , HList y+         )+           => HBetween (HSucc (HSucc x)) z+ where+  hBetween x = hBetween (hPred x) `hAppend` HCons (hPred x) HNil+++-- Set-difference on naturals++class HDiff x y z | x y -> z+ where+  hDiff :: x -> y -> z++instance HDiff HNil x HNil+ where+  hDiff _ _ = HNil++instance ( HOrdMember e y b+         , HDiff x y z+         , HCond b z (HCons e z) z'+         )+           => HDiff (HCons e x) y z'+ where+  hDiff (HCons e x) y = z'+   where z' = hCond b z (HCons e z)+         b  = hOrdMember e y+         z  = hDiff x y+++-- Membership test for types with HOrd instances+-- This special type equality/comparison is entirely pure!++class HOrdMember e l b | e l -> b+ where+  hOrdMember :: e -> l -> b++instance HOrdMember e HNil HFalse+ where+  hOrdMember _ _ = hFalse++instance ( HEq e e' b1+         , HOrdMember e l b2+         , HOr b1 b2 b+         )+           => HOrdMember e (HCons e' l) b+ where+  hOrdMember e (HCons e' l) = hOr b1 b2+   where+    b1 = hEq e e'+    b2 = hOrdMember e l+++{-----------------------------------------------------------------------------}++-- Length operation++class (HList l, HNat n) => HLength l n | l -> n+instance HLength HNil HZero+instance (HLength l n, HNat n, HList l)+      => HLength (HCons a l) (HSucc n)++hLength   :: HLength l n => l -> n+hLength _ =  undefined+++{-----------------------------------------------------------------------------}++-- Bounded lists++class HMaxLength l s+instance (HLength l s', HLt s' (HSucc s) HTrue) => HMaxLength l s++class HMinLength l s+instance (HLength l s', HLt s (HSucc s') HTrue) => HMinLength l s++class HSingleton l+instance HLength l (HSucc HZero) => HSingleton l++hSingle :: (HSingleton l, HHead l e) => l -> e+hSingle = hHead+++{-----------------------------------------------------------------------------}
+ Data/HList/HListPrelude.hs view
@@ -0,0 +1,668 @@+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances,+  UndecidableInstances, FlexibleContexts #-}++{-+   The HList library++   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke++   Basic declarations for typeful heterogeneous lists.+ -}++module Data.HList.HListPrelude where++import Data.HList.FakePrelude++{-----------------------------------------------------------------------------}++-- Heterogeneous type sequences++data HNil      = HNil      deriving (Eq,Show,Read)+data HCons e l = HCons e l deriving (Eq,Show,Read)+++{-----------------------------------------------------------------------------}++-- The set of all types of heterogeneous lists++class HList l+instance HList HNil+instance HList l => HList (HCons e l)+++{-----------------------------------------------------------------------------}++-- Public constructors++hNil  :: HNil+hNil  =  HNil++hCons :: HList l => e -> l -> HCons e l+hCons e l = HCons e l+++{-----------------------------------------------------------------------------}++-- Basic list functions++class HHead l h | l -> h+ where+  hHead :: l -> h++instance HHead (HCons e l) e+ where+  hHead (HCons e _) = e++class HTail l l' | l -> l'+ where+  hTail :: l -> l'++instance HTail (HCons e l) l+ where+  hTail (HCons _ l) = l++++{-----------------------------------------------------------------------------}++-- A class for extension++class HExtend e l l' | e l -> l', l' -> e l+ where+  hExtend :: e -> l -> l'++instance HExtend e HNil (HCons e HNil)+ where+  hExtend e l = HCons e l++instance HList l => HExtend e (HCons e' l) (HCons e (HCons e' l))+ where+  hExtend e l = HCons e l+++{-----------------------------------------------------------------------------}++-- Appending HLists++-- The normal append for comparison++append :: [a] -> [a] -> [a]+append [] l = l+append (x:l) l' = x : append l l'+++-- The class HAppend++class HAppend l l' l'' | l l' -> l''+ where+  hAppend :: l -> l' -> l''+++-- The instance following the normal append++instance HList l => HAppend HNil l l+ where+  hAppend HNil l = l++instance (HList l, HAppend l l' l'')+      => HAppend (HCons x l) l' (HCons x l'')+ where+  hAppend (HCons x l) l' = HCons x (hAppend l l')+++{-----------------------------------------------------------------------------}++-- Reversing HLists++class HReverse l1 l2 | l1 -> l2, l2 -> l1+ where+  hReverse:: l1 -> l2++instance (HReverse' HNil l2 l3, HReverse' HNil l3 l2)+      =>  HReverse l2 l3+ where+  hReverse l1 = hReverse' HNil l1+++-- l3 = (reverse l2) ++ l1++class HReverse' l1 l2 l3 | l1 l2 -> l3+ where+  hReverse':: l1 -> l2 -> l3++instance HReverse' l1 HNil l1+ where+  hReverse' l1 HNil = l1++instance HReverse' (HCons a l1) l2' l3+      => HReverse' l1 (HCons a l2') l3+ where+  hReverse' l1 (HCons a l2') = hReverse' (HCons a l1) l2'+++-- Naive HReverse++class NaiveHReverse l l' | l -> l'+ where+  naiveHReverse :: l -> l'++instance NaiveHReverse HNil HNil+ where+  naiveHReverse HNil = HNil++instance ( NaiveHReverse l l'+         , HAppend l' (HCons e HNil) l''+         )+      =>   NaiveHReverse (HCons e l) l''+ where+  naiveHReverse (HCons e l)+   = hAppend (naiveHReverse l) (HCons e HNil)+++{-----------------------------------------------------------------------------}++--+-- A nicer notation for lists+--++-- List termination+hEnd :: HCons t t1 -> HCons t t1+hEnd t@(HCons _ _) = t++{-+   Note:+        - x :: HCons a b+            means: forall a b. x :: HCons a b+        - hEnd x+            means: exists a b. x :: HCons a b+-}+++-- Building non-empty lists++hBuild   :: (HBuild' HNil a r) => a -> r+hBuild x =  hBuild' HNil x++class HBuild' l a r | r-> a l+ where+  hBuild' :: l -> a -> r++instance HReverse (HCons a l) (HCons a' l')+      => HBuild' l a (HCons a' l')+ where+  hBuild' l x = hReverse (HCons x l)++instance HBuild' (HCons a l) b r+      => HBuild' l a (b->r)+ where+  hBuild' l x y = hBuild' (HCons x l) y++{-++HList> let x = hBuild True in hEnd x+HCons True HNil++HList> let x = hBuild True 'a' in hEnd x+HCons True (HCons 'a' HNil)++HList> let x = hBuild True 'a' "ok" in hEnd x+HCons True (HCons 'a' (HCons "ok" HNil))++HList> hEnd (hBuild (Key 42) (Name "Angus") Cow (Price 75.5))+HCons (Key 42) (HCons (Name "Angus") (HCons Cow (HCons (Price 75.5) HNil)))++HList> hEnd (hBuild (Key 42) (Name "Angus") Cow (Price 75.5)) == angus+True++-}++{-----------------------------------------------------------------------------}++-- A heterogeneous apply operator++class Apply f a r | f a -> r where+  apply :: f -> a -> r+  apply = undefined                     -- In case we use Apply for+                                        -- type-level computations only+++-- Normal function application++instance Apply (x -> y) x y where+  apply f x = f x+++-- Identity++data Id = Id++instance Apply Id x x where+  apply _ x = x+++{-----------------------------------------------------------------------------}++-- A heterogeneous fold for all types++class HList l => HFoldr f v l r | f v l -> r+ where+  hFoldr :: f -> v -> l -> r++instance HFoldr f v HNil v+ where+  hFoldr _ v _ = v++instance ( HFoldr f v l r+         , Apply f (e,r) r'+         )+      => HFoldr f v (HCons e l) r'+ where+  hFoldr f v (HCons e l) = apply f (e,hFoldr f v l)+++{-----------------------------------------------------------------------------}++class HMap f l l' | f l -> l'+ where+  hMap :: f -> l -> l'++instance HMap f HNil HNil+ where+  hMap _ HNil = HNil++instance (+           Apply f x y,+           HMap f xs ys+         )+      => HMap f (HCons x xs) (HCons y ys)+ where+  hMap f (HCons x xs) = HCons (apply f x) (hMap f xs)++{-----------------------------------------------------------------------------}++-- Map a heterogeneous list to a homogeneous one++class HMapOut f r e+ where+  hMapOut :: f -> r -> [e]++instance HMapOut f HNil e+ where+  hMapOut _ _ = []++instance ( HMapOut f l e'+         , Apply f e e'+         )+      =>   HMapOut f (HCons e l) e'+ where+  hMapOut f (HCons e l) = apply f e : hMapOut f l+++{-----------------------------------------------------------------------------}++-- A heterogenous version of mapM.+-- mapM :: forall b m a. (Monad m) => (a -> m b) -> [a] -> m [b]+-- Likewise for mapM_.++hMapM   :: (Monad m, HMapOut f l (m e)) => f -> l -> [m e]+hMapM f =  hMapOut f++-- GHC doesn't like its own type.+-- hMapM_  :: forall m a f e. (Monad m, HMapOut f a (m e)) => f -> a -> m ()+-- Without explicit type signature, it's Ok. Sigh.+-- Anyway, Hugs does insist on a better type. So we restrict as follows:+--+hMapM_   :: (Monad m, HMapOut f l (m ())) => f -> l -> m ()+hMapM_ f =  sequence_ .  disambiguate . hMapM f+ where+  disambiguate :: [q ()] -> [q ()]+  disambiguate =  id+++{-----------------------------------------------------------------------------}++-- A reconstruction of append++append' :: [a] -> [a] -> [a]+append' l l' = foldr (:) l' l++hAppend' :: (HFoldr ApplyHCons v l r) => l -> v -> r+hAppend' l l' = hFoldr ApplyHCons l' l++data ApplyHCons = ApplyHCons++instance HList l => Apply ApplyHCons (e,l) (HCons e l)+ where+  apply ApplyHCons (e,l) = hCons e l+++{-----------------------------------------------------------------------------}++-- A heterogeneous map for all types++data HMap' f = HMap' f++hMap' :: (HFoldr (HMap' f) HNil l r) => f -> l -> r+hMap' f = hFoldr (HMap' f) hNil++instance Apply f e e'+      => Apply (HMap' f) (e,l) (HCons e' l)+ where+  apply (HMap' f) (e,l) = HCons e' l+   where+    e' = apply f e+++{-----------------------------------------------------------------------------}++-- A function for showing++data HShow  = HShow+data HSeq x = HSeq x++instance Show x => Apply HShow x (IO ())+ where+  apply _ x = do putStrLn $ show x++instance ( Monad m+         , Apply f x (m ())+         )+      => Apply (HSeq f) (x,m ()) (m ())+ where+  apply (HSeq f) (x,c) = do apply f x; c+++{-----------------------------------------------------------------------------}++-- Type-level equality for lists++instance HEq HNil HNil HTrue+instance HList l => HEq HNil (HCons e l) HFalse+instance HList l => HEq (HCons e l) HNil HFalse+instance (HList l, HList l', HEq e e' b, HEq l l' b', HAnd b b' b'')+      => HEq (HCons e l) (HCons e' l') b''+++{-----------------------------------------------------------------------------}++-- Staged equality for lists++instance HStagedEq HNil HNil+ where+  hStagedEq _ _ = True++instance HStagedEq HNil (HCons e l)+ where+  hStagedEq _ _ = False++instance HStagedEq (HCons e l) HNil+ where+  hStagedEq _ _ = False++instance ( TypeEq e e' b+         , HStagedEq l l'+         , HStagedEq' b e e'+         )+      =>   HStagedEq (HCons e l) (HCons e' l')+ where+  hStagedEq (HCons e l) (HCons e' l') = (hStagedEq' b e e') && b'+   where+    b  = typeEq e e'+    b' = hStagedEq l l'++class HStagedEq' b e e'+ where+  hStagedEq' :: b -> e -> e' -> Bool++instance HStagedEq' HFalse e e'+ where+  hStagedEq' _ _ _ = False++instance Eq e => HStagedEq' HTrue e e+ where+  hStagedEq' _ = (==)+++{-----------------------------------------------------------------------------}+++-- Ensure a list to contain HNats only++class HList l => HNats l+instance HNats HNil+instance (HNat n, HNats ns) => HNats (HCons n ns)+++-- Static set property based on HEq++class HSet l+instance HSet HNil+instance (HMember e l HFalse, HSet l) => HSet (HCons e l)+++-- Find an element in a set based on HEq+class HNat n => HFind e l n | e l -> n+ where+  hFind :: e -> l -> n++instance ( HEq e e' b+         , HFind' b e l n+         )+      =>   HFind e (HCons e' l) n+ where+  hFind e (HCons e' l) = n+   where+    b  = hEq e e'+    n  = hFind' b e l++class HNat n => HFind' b e l n | b e l -> n+ where+  hFind' :: b -> e -> l -> n++instance HFind' HTrue e l HZero+ where+  hFind' _ _ _ = hZero++instance HFind e l n+      => HFind' HFalse e l (HSucc n)+ where+  hFind' _ e l = hSucc (hFind e l)+++-- Membership test++class HBool b => HMember e l b | e l -> b+instance HMember e HNil HFalse+instance (HEq e e' b, HMember e l b', HOr b b' b'')+      =>  HMember e (HCons e' l) b''++hMember :: HMember e l b => e -> l -> b+hMember _ _ = undefined+++-- Another type-level membership test+-- Check to see if an element e occurs in a list l+-- If not, return HNothing+-- If the element does occur, return HJust l'+-- where l' is a type-level list without e++class HMemberM e l r | e l -> r+instance HMemberM e HNil HNothing+instance (HEq e e' b, HMemberM' b e (HCons e' l) res)+      =>  HMemberM e (HCons e' l) res+class HMemberM' b e l r | b e l -> r+instance HMemberM' HTrue e (HCons e l) (HJust l)+instance (HMemberM e l r, HMemberM' r e (HCons e' l) res)+    => HMemberM' HFalse e (HCons e' l) res+instance HMemberM' HNothing e l HNothing+instance HMemberM' (HJust l') e (HCons e' l) (HJust (HCons e' l'))++++-- Membership test based on type equality++class HBool b => HTMember e l b | e l -> b+instance HTMember e HNil HFalse+instance (TypeEq e e' b, HTMember e l b', HOr b b' b'')+      =>  HTMember e (HCons e' l) b''++hTMember :: HTMember e l b => e -> l -> b+hTMember _ _ = undefined+++-- Intersection based on HTMember++class HTIntersect l1 l2 l3 | l1 l2 -> l3+ where+  hTIntersect :: l1 -> l2 -> l3++instance HTIntersect HNil l HNil+ where+  hTIntersect _ _ = HNil++instance ( HTMember h l1 b+         , HTIntersectBool b h t l1 l2+         )+         => HTIntersect (HCons h t) l1 l2+ where+  hTIntersect (HCons h t) l1 = hTIntersectBool b h t l1+   where+    b = hTMember h l1++class HBool b => HTIntersectBool b h t l1 l2 | b h t l1 -> l2+ where+ hTIntersectBool :: b -> h -> t -> l1 -> l2++instance HTIntersect t l1 l2+      => HTIntersectBool HTrue h t l1 (HCons h l2)+ where+  hTIntersectBool _ h t l1 = HCons h (hTIntersect t l1)++instance HTIntersect t l1 l2+      => HTIntersectBool HFalse h t l1 l2+ where+  hTIntersectBool _ _ t l1 = hTIntersect t l1+++-- Turn a heterogeneous list into a homogeneous one++class HList2List l e+ where+  hList2List :: l -> [e]++instance HList2List HNil e+ where+  hList2List HNil = []++instance HList2List l e+      => HList2List (HCons e l) e+ where+  hList2List (HCons e l) = e:hList2List l+++{-----------------------------------------------------------------------------}++-- Turn list in a list of justs++class ToHJust l l' | l -> l'+ where+  toHJust :: l -> l'++instance ToHJust HNil HNil+ where+  toHJust HNil = HNil++instance ToHJust l l' => ToHJust (HCons e l) (HCons (HJust e) l')+ where+  toHJust (HCons e l) = HCons (HJust e) (toHJust l)+++{-----------------------------------------------------------------------------}++-- Extract justs from list of maybes++class FromHJust l l' | l -> l'+ where+  fromHJust :: l -> l'++instance FromHJust HNil HNil+ where+  fromHJust HNil = HNil++instance FromHJust l l' => FromHJust (HCons HNothing l) l'+ where+  fromHJust (HCons _ l) = fromHJust l++instance FromHJust l l' => FromHJust (HCons (HJust e) l) (HCons e l')+ where+  fromHJust (HCons (HJust e) l) = HCons e (fromHJust l)+++{-----------------------------------------------------------------------------}++-- Annotated lists++data HAddTag t = HAddTag t+data HRmTag    = HRmTag++hAddTag :: (HMap (HAddTag t) l l') => t -> l -> l'+hAddTag t l = hMap (HAddTag t) l+hRmTag :: (HMap HRmTag l l') => l -> l'+hRmTag l    = hMap HRmTag l++instance Apply (HAddTag t) e (e,t)+ where+  apply (HAddTag t) e = (e,t)++instance Apply HRmTag (e,t) e+ where+  apply HRmTag (e,_) = e+++-- Annotate list with a type-level Boolean+hFlag :: (HMap (HAddTag HTrue) l l') => l -> l'+hFlag l = hAddTag hTrue l+++{-----------------------------------------------------------------------------}++-- Splitting by HTrue and HFalse++class HSplit l l' l'' | l -> l' l''+ where+  hSplit :: l -> (l',l'')++instance HSplit HNil HNil HNil+ where+  hSplit HNil = (HNil,HNil)++instance HSplit l l' l''+      => HSplit (HCons (e,HTrue) l) (HCons e l') l''+ where+  hSplit (HCons (e,_) l) = (HCons e l',l'')+   where+    (l',l'') = hSplit l++instance HSplit l l' l''+      => HSplit (HCons (e,HFalse) l) l' (HCons e l'')+ where+  hSplit (HCons (e,_) l) = (l',HCons e l'')+   where+    (l',l'') = hSplit l++{-++Let expansion makes a difference to Hugs:++HListPrelude> let x = (hFlag (HCons "1" HNil)) in hSplit x+(HCons "1" HNil,HNil)+HListPrelude> hSplit (hFlag (HCons "1" HNil))+ERROR - Unresolved overloading+*** Type       : HSplit (HCons ([Char],HTrue) HNil) a b => (a,b)+*** Expression : hSplit (hFlag (HCons "1" HNil))+++-}+++{-----------------------------------------------------------------------------}
+ Data/HList/HOccurs.hs view
@@ -0,0 +1,231 @@+{-# LANGUAGE EmptyDataDecls, MultiParamTypeClasses, FlexibleInstances,+  FlexibleContexts, UndecidableInstances #-}++{-+   The HList library++   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke++   Result-type-driven operations on typeful heterogeneous lists.+-}++module Data.HList.HOccurs where++import Data.HList.FakePrelude+import Data.HList.HListPrelude++{-----------------------------------------------------------------------------}++-- Zero or more occurrences++class HOccursMany e l+ where+  hOccursMany :: l -> [e]++instance HOccursMany e HNil+ where+  hOccursMany HNil = []++instance ( HOccursMany e l, HList l )+      =>   HOccursMany e (HCons e l)+ where+  hOccursMany (HCons e l) = e:hOccursMany l++instance ( HOccursMany e l, HList l )+      =>   HOccursMany e (HCons e' l)+ where+  hOccursMany (HCons _ l) = hOccursMany l+++{-----------------------------------------------------------------------------}++-- One or more occurrences++class HOccursMany1 e l+ where+  hOccursMany1 :: l -> (e,[e])++instance ( HOccursMany e l, HList l )+      =>   HOccursMany1 e (HCons e l)+ where+  hOccursMany1 (HCons e l) = (e,hOccursMany l)++instance ( HOccursMany1 e l, HList l )+      => HOccursMany1 e (HCons e' l)+ where+  hOccursMany1 (HCons _ l) = hOccursMany1 l+++{-----------------------------------------------------------------------------}++-- The first occurrence++class HOccursFst e l+ where+  hOccursFst :: l -> e++instance HList l+      => HOccursFst e (HCons e l)+ where+  hOccursFst (HCons e _) = e++instance ( HOccursFst e l, HList l )+      =>   HOccursFst e (HCons e' l)+ where+  hOccursFst (HCons _ l) = hOccursFst l+++{-----------------------------------------------------------------------------}++-- One occurrence and nothing is left++class HOccurs e l+ where+  hOccurs :: l -> e++data TypeNotFound e++instance Fail (TypeNotFound e)+      => HOccurs e HNil+ where+  hOccurs = undefined++instance ( HList l+         , HOccursNot e l+         )+           => HOccurs e (HCons e l)+ where+  hOccurs (HCons e _) = e++instance ( HOccurs e l+         , HList l+         )+           => HOccurs e (HCons e' l)+ where+  hOccurs (HCons _ l) = hOccurs l+++{-----------------------------------------------------------------------------}++-- One occurrence and nothing is left+-- A variation that avoids overlapping instances++class HOccurs' e l+ where+  hOccurs' :: l -> e++instance ( TypeEq e e' b+         , HOccursBool b e (HCons e' l) )+      =>   HOccurs' e (HCons e' l)+ where+  hOccurs' (HCons e' l) = e+   where+    e = hOccursBool b (HCons e' l)+    b = proxyEq (toProxy e) (toProxy e')++class HOccursBool b e l+ where+  hOccursBool :: b -> l -> e++instance ( HList l+         , HOccursNot e l+         )+           => HOccursBool HTrue e (HCons e l)+ where+  hOccursBool _ (HCons e _) = e++instance ( HOccurs' e l+         , HList l+         )+           => HOccursBool HFalse e (HCons e' l)+ where+  hOccursBool _ (HCons _ l) = hOccurs' l+++{-----------------------------------------------------------------------------}++-- Zero or at least one occurrence++class HOccursOpt e l+ where+  hOccursOpt :: l -> Maybe e++instance HOccursOpt e HNil+ where+  hOccursOpt HNil = Nothing++instance HOccursOpt e (HCons e l)+ where+  hOccursOpt (HCons e _) = Just e++instance HOccursOpt e l+      => HOccursOpt e (HCons e' l)+ where+  hOccursOpt (HCons _ l) = hOccursOpt l+++{-----------------------------------------------------------------------------}++-- Class to test that a type is "free" in a type sequence++data TypeFound e+class HOccursNot e l+instance HOccursNot e HNil+instance Fail (TypeFound e) => HOccursNot e (HCons e l)+instance HOccursNot e l => HOccursNot e (HCons e' l)+++{-----------------------------------------------------------------------------}++class HProject l l'+ where+  hProject :: l -> l'++instance HProject l HNil+ where+  hProject _ = HNil++instance ( HList l'+         , HOccurs e l+         , HProject l l'+         )+      =>   HProject l (HCons e l')+ where+  hProject l = HCons (hOccurs l) (hProject l)+++{-----------------------------------------------------------------------------}++-- Illustration of typical test scenarios++{-++Retrieve the Breed of an animal.++ghci-or-hugs> hOccurs myAnimal :: Breed+Cow++-}++{-++Normal hOccurs requires specification of the result type even if the result+type is determined by the fact that we are faced with a singleton list.++ghci-or-hugs> hOccurs (HCons 1 HNil)++<interactive>:1:+    No instance for (HOccurs e1 (HCons e HNil))++-}++{-++However, hOccurs can be elaborated as improved as follows:++ghci-or-hugs> hLookup (HCons 1 HNil)+1++-}++{-----------------------------------------------------------------------------}
+ Data/HList/HTypeIndexed.hs view
@@ -0,0 +1,124 @@+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances,+  UndecidableInstances, FlexibleContexts #-}++{-+   The HList library++   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke++   Type-indexed operations on typeful heterogeneous lists.+-}++module Data.HList.HTypeIndexed where++import Data.HList.FakePrelude+import Data.HList.HListPrelude+import Data.HList.HArray+import Data.HList.HOccurs+++{-----------------------------------------------------------------------------}++class HDeleteMany e l l' | e l -> l'+ where+  hDeleteMany :: Proxy e -> l -> l'++instance HDeleteMany e HNil HNil+ where+  hDeleteMany _ HNil = HNil++instance ( HList l+         , TypeEq e e' b+         , HDeleteManyCase b e e' l l'+         )+      =>   HDeleteMany e (HCons e' l) l'+ where+  hDeleteMany p (HCons e' l) = l'+   where+    b  = proxyEq p (toProxy e')+    l' = hDeleteManyCase b p e' l++class HDeleteManyCase b e e' l l' | b e e' l -> l'+ where+  hDeleteManyCase :: b -> Proxy e -> e' -> l -> l'++instance HDeleteMany e l l'+      => HDeleteManyCase HTrue e e l l'+ where+  hDeleteManyCase _ p _ l = hDeleteMany p l+++instance HDeleteMany e l l'+      => HDeleteManyCase HFalse e e' l (HCons e' l')+ where+  hDeleteManyCase _ p e' l = HCons e' (hDeleteMany p l)+++{-----------------------------------------------------------------------------}++-- Map a type to a natural++class HNat n => HType2HNat e l n | e l -> n+instance (TypeEq e' e b, HType2HNatCase b e l n)+      =>  HType2HNat e (HCons e' l) n++-- Helper class++class (HBool b, HNat n) => HType2HNatCase b e l n | b e l -> n+instance HOccursNot e l => HType2HNatCase HTrue e l HZero+instance HType2HNat e l n => HType2HNatCase HFalse e l (HSucc n)++hType2HNat :: HType2HNat e l n => Proxy e -> l -> n+hType2HNat _ _ = undefined++++-- Map types to naturals++class HTypes2HNats ps l ns | ps l -> ns+ where+  hTypes2HNats :: ps -> l -> ns++instance HTypes2HNats HNil l HNil+ where+  hTypes2HNats _ _ = HNil++instance ( HType2HNat   e l n+         , HTypes2HNats ps l ns+         )+      =>   HTypes2HNats (HCons (Proxy e) ps) l (HCons n ns)+ where+  hTypes2HNats (HCons p ps) l = HCons (hType2HNat p l) (hTypes2HNats ps l)+++{-----------------------------------------------------------------------------}++-- Define type-indexed delete in terms of the natural-based primitive+hDeleteAtProxy :: (HDeleteAtHNat n l l', HType2HNat e l n) => Proxy e -> l -> l'+hDeleteAtProxy p l = hDeleteAtHNat (hType2HNat p l) l+++{-----------------------------------------------------------------------------}++-- Define type-indexed update in terms of the natural-based update+hUpdateAtType :: (HUpdateAtHNat n e l l', HType2HNat e l n) => e -> l -> l'+hUpdateAtType e l = hUpdateAtHNat (hType2HNat (toProxy e) l) e l+++{-----------------------------------------------------------------------------}++-- Projection based on proxies+hProjectByProxies :: (HProjectByHNats ns l l', HTypes2HNats ps l ns) => ps -> l -> l'+hProjectByProxies ps l = hProjectByHNats (hTypes2HNats ps l) l+++{-----------------------------------------------------------------------------}++-- Splitting based on proxies+hSplitByProxies :: (HMap (HAddTag HTrue) l l', HSplitByHNats' ns l' l'1 l'',+                   HTypes2HNats ps l ns) =>+                  ps -> l -> (l'1, l'')+hSplitByProxies ps l = hSplitByHNats (hTypes2HNats ps l) l+++{-----------------------------------------------------------------------------}
+ Data/HList/HZip.hs view
@@ -0,0 +1,84 @@+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances #-}++module Data.HList.HZip where++import Data.HList.HListPrelude++{-+   The HList library++   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke++   Zipping and unzipping for (conceptually) lists of pairs.+ -}++{-----------------------------------------------------------------------------}++-- Test for zippability++class HZippable x y+instance HZippable HNil HNil+instance HZippable l l' => HZippable (HCons e l) (HCons e' l')+++{-----------------------------------------------------------------------------}++-- Zip and unzip++class HZip x y l | x y -> l, l -> x y+ where+  hZip   :: x -> y -> l+  hUnzip :: l -> (x,y)++{-++-- Zipping version I+-- Somehow too polymorphic.+-- Version II specialises for HNil and HCons.++instance HZippable x y => HZip x y (x,y)+ where+  hZip x y = (x,y)+  hUnzip = id++-}++{-++-- Zipping version II+-- Built-in show and alias-based type construction inconvenient.+-- Version III goes for a true list of pairs.++instance HZip HNil HNil (HNil,HNil)+ where+  hZip x y = (x,y)+  hUnzip = id++instance HZip xt yt zt+      => HZip (HCons xh xt) (HCons yh yt) (HCons xh xt,HCons yh yt)+ where+  hZip x y = (x,y)+  hUnzip = id++-}+++-- {-++--- Zipping version III+--- Works best for us.++instance HZip HNil HNil HNil+ where+  hZip HNil HNil = HNil+  hUnzip HNil = (HNil,HNil)++instance HZip tx ty l+      => HZip (HCons hx tx) (HCons hy ty) (HCons (hx,hy) l)+ where+  hZip (HCons hx tx) (HCons hy ty) = HCons (hx,hy) (hZip tx ty)+  hUnzip (HCons (hx,hy) l) = (HCons hx tx, HCons hy ty)+   where+    (tx,ty) = hUnzip l++-- -}
+ Data/HList/Label4.hs view
@@ -0,0 +1,39 @@+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, UndecidableInstances, EmptyDataDecls #-}+{-+   The HList library++   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke++   Yet another model of labels.+   Labels are type proxies.+-}++module Data.HList.Label4 where++import Data.Typeable+import Data.Char++import Data.HList.FakePrelude+import Data.HList.Record+++-- Equality on labels++instance TypeEq x y b => HEq (Proxy x) (Proxy y) b+++-- Show label++instance Typeable x => ShowLabel (Proxy x)+ where+  showLabel = (\(x:xs) -> toLower x:xs)+            . reverse+            . takeWhile (not . (==) '.')+            . reverse+            . show+{-+            . tyConString+            . typeRepTyCon+-}+            . typeOf+            . unProxy
+ Data/HList/Record.hs view
@@ -0,0 +1,394 @@+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances,+  FlexibleContexts, UndecidableInstances #-}+{-# OPTIONS -fglasgow-exts #-}++{-+   The HList library++   (C) 2004-2006, Oleg Kiselyov, Ralf Laemmel, Keean Schupke++   Extensible records++   The are different models of labels that go with this module;+   see the files Label?.hs.+-}++module Data.HList.Record where++import Data.HList.FakePrelude+import Data.HList.HListPrelude+import Data.HList.HArray+++{-----------------------------------------------------------------------------}++-- Record types as label-value pairs, where label is purely phantom.+-- Thus the run-time representation of a field is the same as that of+-- its value, and the record, at run-time, is indistinguishable from+-- the HList of field values. At run-time, all information about the+-- labels is erased.++-- Field of label l with value type v+newtype LVPair l v = LVPair { valueLVPair :: v }++-- Label accessor+labelLVPair :: LVPair l v -> l+labelLVPair = undefined++newLVPair :: l -> v -> LVPair l v+newLVPair _ = LVPair++newtype Record r = Record r+++-- Build a record+mkRecord :: HRLabelSet r => r -> Record r+mkRecord = Record+++-- Build an empty record+emptyRecord :: Record HNil+emptyRecord = mkRecord HNil+++-- Propery of a proper label set for a record: no duplication of labels++class HRLabelSet ps+instance HRLabelSet HNil+instance HRLabelSet (HCons x HNil)+instance ( HEq l1 l2 HFalse+         , HRLabelSet (HCons (LVPair l2 v2) r)+         , HRLabelSet (HCons (LVPair l1 v1) r)+         ) => HRLabelSet (HCons (LVPair l1 v1) (HCons (LVPair l2 v2) r))++{-+instance (HZip ls vs ps, HLabelSet ls) => HRLabelSet ps+-}++class HLabelSet ls+instance HLabelSet HNil+instance (HMember x ls HFalse, HLabelSet ls)+      =>  HLabelSet (HCons x ls)+++-- Construct the (phantom) list of labels of the record.+-- This is a type-level only function+class RecordLabels r ls | r -> ls+instance RecordLabels HNil HNil+instance RecordLabels r' ls+      => RecordLabels (HCons (LVPair l v) r') (HCons l ls)++recordLabels :: RecordLabels r ls => r -> ls+recordLabels = undefined+++{-----------------------------------------------------------------------------}++-- A Show instance to appeal to normal records++instance ShowComponents r => Show (Record r)+ where+  show (Record r) =  "Record{"+                  ++ showComponents "" r+                  ++ "}"++class ShowComponents l+ where+  showComponents :: String -> l -> String++instance ShowComponents HNil+ where+  showComponents _ HNil = ""++instance ( ShowLabel l+         , Show v+         , ShowComponents r+         )+      =>   ShowComponents (HCons (LVPair l v) r)+ where+  showComponents comma (HCons f@(LVPair v) r)+     =  comma+     ++ showLabel (labelLVPair f)+     ++ "="+     ++ show v+     ++ showComponents "," r++class ShowLabel l+ where+  showLabel :: l -> String+++{-----------------------------------------------------------------------------}++-- Extension for records++instance HRLabelSet (HCons (LVPair l v) r)+    => HExtend (LVPair l v) (Record r) (Record (HCons (LVPair l v) r))+ where+  hExtend f (Record r) = mkRecord (HCons f r)+++{-----------------------------------------------------------------------------}++-- Record concatenation++instance ( HRLabelSet r''+         , HAppend r r' r''+         )+    => HAppend (Record r) (Record r') (Record r'')+ where+  hAppend (Record r) (Record r') = mkRecord (hAppend r r')+++{-----------------------------------------------------------------------------}++-- Lookup operation++-- This is a baseline implementation.+-- We use a helper class, HasField, to abstract from the implementation.++class HasField l r v | l r -> v+  where+    hLookupByLabel:: l -> r -> v++{-+instance ( RecordLabels r ls+         , HFind l ls n+         , HLookupByHNat n r (LVPair l v)+         ) => HasField l (Record r) v+  where+    hLookupByLabel l (Record r) = v+      where+        ls = recordLabels r+        n = hFind l ls+        (LVPair v) = hLookupByHNat n r++-}+++-- Because hLookupByLabel is so frequent and important, we implement+-- it separately, more efficiently. The algorithm is familiar assq, only+-- the comparison operation is done at compile-time++instance HasField l r v => HasField l (Record r) v where+    hLookupByLabel l (Record r) = hLookupByLabel l r++class HasField' b l r v | b l r -> v where+    hLookupByLabel':: b -> l -> r -> v++instance (HEq l l' b, HasField' b l (HCons (LVPair l' v') r) v)+    => HasField l (HCons (LVPair l' v') r) v where+    hLookupByLabel l r@(HCons f' _) =+             hLookupByLabel' (hEq l (labelLVPair f')) l r++instance HasField' HTrue l (HCons (LVPair l v) r) v where+    hLookupByLabel' _ _ (HCons (LVPair v) _) = v+instance HasField l r v => HasField' HFalse l (HCons fld r) v where+    hLookupByLabel' _ l (HCons _ r) = hLookupByLabel l r++++{-----------------------------------------------------------------------------}++-- Delete operation+hDeleteAtLabel :: (H2ProjectByLabels (HCons e HNil) t t1 t2) => e -> Record t -> Record t2+hDeleteAtLabel l (Record r) = Record r'+ where+  (_,r')  = h2projectByLabels (HCons l HNil) r+++{-----------------------------------------------------------------------------}++-- Update operation+hUpdateAtLabel ::( RecordLabels t ls, HFind e ls n, HUpdateAtHNat n (LVPair e v) t l') =>+                e -> v -> Record t -> Record l'+hUpdateAtLabel l v (Record r) = Record r'+ where+  n    = hFind l (recordLabels r)+  r'   = hUpdateAtHNat n (newLVPair l v) r+++{-----------------------------------------------------------------------------}+-- Projection for records+-- It is also an important operation: the basis of many+-- deconstructors -- so we try to implement it efficiently.+hProjectByLabels :: (HRLabelSet a, H2ProjectByLabels ls t a b) => ls -> Record t -> Record a+hProjectByLabels ls (Record r) = mkRecord (fst $ h2projectByLabels ls r)++hProjectByLabels2 :: (HRLabelSet t2, HRLabelSet t1, H2ProjectByLabels ls t t1 t2) =>+                                                 ls -> Record t -> (Record t1, Record t2)+hProjectByLabels2 ls (Record r) = (mkRecord rin, mkRecord rout)+   where (rin,rout) = h2projectByLabels ls r++-- Invariant: r = rin `disjoint-union` rout+--            labels(rin) = ls+class H2ProjectByLabels ls r rin rout | ls r -> rin rout where+    h2projectByLabels :: ls -> r -> (rin,rout)++instance H2ProjectByLabels HNil r HNil r where+    h2projectByLabels _ r = (HNil,r)++instance H2ProjectByLabels (HCons l ls) HNil HNil HNil where+    h2projectByLabels _ _ = (HNil,HNil)++instance (HMemberM l' (HCons l ls) b,+          H2ProjectByLabels' b (HCons l ls) (HCons (LVPair l' v') r') rin rout)+    => H2ProjectByLabels (HCons l ls) (HCons (LVPair l' v') r') rin rout where+    -- h2projectByLabels = h2projectByLabels' (undefined::b)+    -- The latter is solely for the Hugs benefit+    h2projectByLabels ls r@(HCons _ _) =h2projectByLabels' (undefined::b) ls r+      -- where b = hMember (labelLVPair f') ls++class H2ProjectByLabels' b ls r rin rout | b ls r -> rin rout where+    h2projectByLabels' :: b -> ls -> r -> (rin,rout)++instance H2ProjectByLabels ls' r' rin rout =>+    H2ProjectByLabels' (HJust ls') ls (HCons f' r') (HCons f' rin) rout where+    h2projectByLabels' _ _ (HCons x r) = (HCons x rin, rout)+        where (rin,rout) = h2projectByLabels (undefined::ls') r++instance H2ProjectByLabels ls r' rin rout =>+    H2ProjectByLabels' HNothing ls (HCons f' r') rin (HCons f' rout) where+    h2projectByLabels' _ ls (HCons x r) = (rin, HCons x rout)+        where (rin,rout) = h2projectByLabels ls r+++{-----------------------------------------------------------------------------}++-- Rename the label of record+hRenameLabel :: (H2ProjectByLabels (HCons e HNil) t t1 t2, HasField e t v,+                HRLabelSet (HCons (LVPair l v) t2)) =>+               e -> l -> Record t -> Record (HCons (LVPair l v) t2)+hRenameLabel l l' r = r''+ where+  v   = hLookupByLabel l r+  r'  = hDeleteAtLabel l r+  r'' = hExtend (newLVPair l' v) r'+++{-----------------------------------------------------------------------------}++-- A variation on update: type-preserving update.+hTPupdateAtLabel :: (HUpdateAtHNat n (LVPair l a) t l', HFind l ls n, RecordLabels t ls,+                    HasField l t a) =>+                   l -> a -> Record t -> Record l'+hTPupdateAtLabel l v r = hUpdateAtLabel l v r+ where+   te :: a -> a -> ()+   te _ _ = ()+   _ = te v (hLookupByLabel l r)++{-++-- We could also say:++hTPupdateAtLabel l v r = hUpdateAtLabel l v r `asTypeOf` r++-- Then we were taking a dependency on Haskell's type equivalence.+-- This would also constrain the actual implementation of hUpdateAtLabel.++-}++{-----------------------------------------------------------------------------}++-- Subtyping for records++instance ( RecordLabels r' ls+         , H2ProjectByLabels ls r r' rout+         )+    => SubType (Record r) (Record r')+++{-----------------------------------------------------------------------------}++class  HLeftUnion r r' r'' | r r' -> r''+ where hLeftUnion :: r -> r' -> r''++instance HLeftUnion r (Record HNil) r+ where   hLeftUnion r _ = r++instance ( RecordLabels r ls+         , HMember l ls b+         , HLeftUnionBool b r (LVPair l v) r'''+         , HLeftUnion (Record r''') (Record r') r''+         )+           => HLeftUnion (Record r) (Record (HCons (LVPair l v) r')) r''+  where+   hLeftUnion (Record r) (Record (HCons f r')) = r''+    where+     b       = hMember (labelLVPair f) (recordLabels r)+     r'''    = hLeftUnionBool b r f+     r''     = hLeftUnion (Record r''') (Record r')++class  HLeftUnionBool b r f r' | b r f -> r'+ where hLeftUnionBool :: b -> r -> f -> r'++instance HLeftUnionBool HTrue r f r+   where hLeftUnionBool _ r _  = r++instance HLeftUnionBool HFalse r f (HCons f r)+   where hLeftUnionBool _ r f = HCons f r+++{-----------------------------------------------------------------------------}+-- Compute the symmetric union of two records r1 and r2 and+-- return the pair of records injected into the union (ru1, ru2).+-- To be more precise, we compute the symmetric union _type_ ru+-- of two record _types_ r1 and r2. The emphasis on types is important.+-- The two records (ru1,ru2) in the result of unionSR have the same+-- type ru, but they are generally different values.+-- Here the simple example: suppose+--   r1 = (Label .=. True)  .*. emptyRecord+--   r2 = (Label .=. False) .*. emptyRecord+-- Then unionSR r1 r2 will return (r1,r2). Both components of the result+-- are different records of the same type.++-- To project from the union ru, use hProjectByLabels.+-- It is possible to project from the union obtaining a record+-- that was not used at all when creating the union.+-- We do assure however that if (unionSR r1 r2) gave (r1u,r2u),+-- then projecting r1u onto the type of r1 gives the _value_ identical+-- to r1. Ditto for r2.++class UnionSymRec r1 r2 ru | r1 r2 -> ru where+    unionSR :: r1 -> r2 -> (ru, ru)++instance UnionSymRec r1 (Record HNil) r1 where+    unionSR r1 _ = (r1, r1)++instance ( RecordLabels r1 ls+         , HMember l ls b+         , UnionSymRec' b (Record r1) (LVPair l v) (Record r2') ru+         )+    => UnionSymRec (Record r1) (Record (HCons (LVPair l v) r2')) ru+    where+    unionSR r1 (Record (HCons f r2')) =+        unionSR' (undefined::b) r1 f (Record r2')++class UnionSymRec' b r1 f2 r2' ru | b r1 f2 r2' -> ru where+    unionSR' :: b -> r1 -> f2 -> r2'  -> (ru, ru)++-- Field f2 is already in r1, so it will be in the union of r1+-- with the rest of r2.+-- To inject (HCons f2 r2) in that union, we should replace the+-- field f2+instance (UnionSymRec r1 r2' (Record ru),+          HasField l2 ru v2,+          HUpdateAtHNat n (LVPair l2 v2) ru ru,+          RecordLabels ru ls,+          HFind l2 ls n)+    => UnionSymRec' HTrue r1 (LVPair l2 v2) r2' (Record ru) where+    unionSR' _ r1 (LVPair v2) r2' = (ul, ur')+       where (ul,ur) = unionSR r1 r2'+             ur' = hTPupdateAtLabel (undefined::l2) v2 ur+++instance (UnionSymRec r1 r2' (Record ru),+          HExtend f2 (Record ru) (Record (HCons f2 ru)))+    => UnionSymRec' HFalse r1 f2 r2' (Record (HCons f2 ru)) where+    unionSR' _ r1 f2 r2' = (ul', ur')+       where (ul,ur) = unionSR r1 r2'+             ul' = hExtend f2 ul+             ur' = hExtend f2 ur++
+ Data/HList/TIC.hs view
@@ -0,0 +1,74 @@+{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}++{-+   The HList library++   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke++   Type-indexed co-products.+-}++module Data.HList.TIC where++import Data.Dynamic++import Data.HList.FakePrelude+import Data.HList.HListPrelude+import Data.HList.HOccurs+import Data.HList.TIP+++{-----------------------------------------------------------------------------}++-- A datatype for type-indexed co-products++data TIC l = TIC Dynamic+++{-----------------------------------------------------------------------------}++-- Public constructor++mkTIC :: ( HTypeIndexed l+         , HTypeProxied l+         , HOccurs (Proxy i) l+         , Typeable i+         )+      => i -> TIC l++mkTIC i = TIC (toDyn i)+++{-----------------------------------------------------------------------------}++-- Public destructor++unTIC :: ( HTypeIndexed l+         , HTypeProxied l+         , HOccurs (Proxy o) l+         , Typeable o+         )+      => TIC l -> Maybe o++unTIC (TIC i) = fromDynamic i+++{-----------------------------------------------------------------------------}++-- A type-indexed type sequence that is a sequence of proxy types++class HTypeProxied l+instance HTypeProxied HNil+instance HTypeProxied l => HTypeProxied (HCons (Proxy e) l)+++{-----------------------------------------------------------------------------}++-- TICs are opaque++instance Show (TIC l)+ where+  show _ = "<Cannot show TIC content!>"+++{-----------------------------------------------------------------------------}
+ Data/HList/TIP.hs view
@@ -0,0 +1,254 @@+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, FlexibleContexts, UndecidableInstances #-}+module Data.HList.TIP where++{-+   The HList library++   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke++   Type-indexed products.+-}++import Data.HList.FakePrelude+import Data.HList.HListPrelude+import Data.HList.HArray+import Data.HList.HOccurs+import Data.HList.HTypeIndexed+++{-----------------------------------------------------------------------------}++-- The newtype for type-indexed products++newtype TIP l = TIP l+        deriving (Read,Show)++mkTIP :: HTypeIndexed l => l -> TIP l+mkTIP = TIP++unTIP :: TIP l -> l+unTIP (TIP l) = l++emptyTIP :: TIP HNil+emptyTIP = mkTIP HNil++++{-----------------------------------------------------------------------------}++-- Type-indexed type sequences++class HList l => HTypeIndexed l+instance HTypeIndexed HNil+instance (HOccursNot e l,HTypeIndexed l) => HTypeIndexed (HCons e l)+++{-----------------------------------------------------------------------------}++--+-- One occurrence and nothing is left+--+-- This variation provides an extra feature for singleton lists.+-- That is, the result type is unified with the element in the list.+-- Hence the explicit provision of a result type can be omitted.+--++instance TypeCast e' e => HOccurs e (TIP (HCons e' HNil))+ where+  hOccurs (TIP (HCons e' _)) = typeCast e'++instance HOccurs e (HCons x (HCons y l))+      => HOccurs e (TIP (HCons x (HCons y l)))+ where+  hOccurs (TIP l) = hOccurs l+++{-----------------------------------------------------------------------------}++-- HOccursNot lifted to TIPs++instance HOccursNot e l => HOccursNot e (TIP l)+++{-----------------------------------------------------------------------------}++-- Type-indexed extension+hExtend' :: (HTypeIndexed t, HOccursNot e t) => e -> TIP t -> TIP (HCons e t)+hExtend' e (TIP l) = mkTIP (HCons e l)++{-++Valid type I++hExtend' :: (HTypeIndexed l, HOccursNot e l)+         => e -> TIP l -> TIP (HCons e l)++Valid type II++*TIP> :t hExtend'+hExtend' :: forall l e.+            (HTypeIndexed (HCons e l)) =>+            e -> TIP l -> TIP (HCons e l)++-}+++{-----------------------------------------------------------------------------}++-- Lift extension through HExtend++instance ( HOccursNot e l+         , HTypeIndexed l+         )+      => HExtend e (TIP l) (TIP (HCons e l))+ where+  hExtend = hExtend'+++{-----------------------------------------------------------------------------}++-- Lifting previous operations+++instance ( HAppend l l' l''+         , HTypeIndexed l''+         )+           => HAppend (TIP l) (TIP l') (TIP l'')+ where+  hAppend (TIP l) (TIP l') = mkTIP (hAppend l l')+++instance HOccursMany e l+      => HOccursMany e (TIP l)+ where+  hOccursMany = hOccursMany . unTIP+++instance HOccursMany1 e l+      => HOccursMany1 e (TIP l)+ where+  hOccursMany1 = hOccursMany1 . unTIP+++instance HOccursFst e l+      => HOccursFst e (TIP l)+ where+  hOccursFst = hOccursFst . unTIP+++instance HOccursOpt e l+      => HOccursOpt e (TIP l)+ where+  hOccursOpt = hOccursOpt . unTIP+++{-----------------------------------------------------------------------------}++-- Shielding type-indexed operations++onTIP :: HTypeIndexed a => (b -> a) -> TIP b -> TIP a+onTIP f (TIP l) = mkTIP (f l)++tipyDelete :: (HTypeIndexed l',HType2HNat e b n,HDeleteAtHNat n b l') => Proxy e -> TIP b -> TIP l'+tipyDelete  p t  = onTIP (hDeleteAtProxy p) t+tipyUpdate :: (HTypeIndexed l',HType2HNat e b n,HUpdateAtHNat n e b l') => e -> TIP b -> TIP l'+tipyUpdate  e t  = onTIP (hUpdateAtType e) t+tipyProject :: (HTypeIndexed l',HTypes2HNats ps b ns,HProjectByHNats ns b l') => ps -> TIP b -> TIP l'+tipyProject ps t = onTIP (hProjectByProxies ps) t+++-- Split produces two TIPs+tipySplit :: (HTypeIndexed t2,HTypeIndexed t1,HTypes2HNats ps t ns,HSplitByHNats' ns l' t1 t2,+             HMap (HAddTag HTrue) t l') =>+            ps -> TIP t -> (TIP t1, TIP t2)+tipySplit ps (TIP l) = (mkTIP l',mkTIP l'')+ where+  (l',l'') = hSplitByProxies ps l+++{-----------------------------------------------------------------------------}++-- Subtyping for TIPs++instance SubType (TIP l) (TIP HNil)+instance (HOccurs e l, SubType (TIP l) (TIP l'))+      =>  SubType (TIP l) (TIP (HCons e l'))+++{-----------------------------------------------------------------------------}++-- Sample code++{-++Assume++myTipyCow = TIP myAnimal++animalKey :: (HOccurs Key l, SubType l (TIP Animal)) => l -> Key+animalKey = hOccurs++Session log++*TIP> :t myTipyCow+myTipyCow :: TIP Animal++*TIP> hOccurs myTipyCow :: Breed+Cow++*TIP> hExtend BSE myTipyCow+TIP (HCons BSE+    (HCons (Key 42)+    (HCons (Name "Angus")+    (HCons Cow+    (HCons (Price 75.5)+     HNil)))))++*TIP> BSE .*. myTipyCow+--- same as before ---++*TIP> Sheep .*. myTipyCow+Type error ...++*TIP> Sheep .*. tipyDelete myTipyCow (HProxy::HProxy Breed)+TIP (HCons Sheep (HCons (Key 42) (HCons (Name "Angus") (HCons (Price 75.5) HNil))))++*TIP> tipyUpdate myTipyCow Sheep+TIP (HCons (Key 42) (HCons (Name "Angus") (HCons Sheep (HCons (Price 75.5) HNil))))++-}++{-----------------------------------------------------------------------------}++-- This example from the TIR paper challenges singleton lists.+-- Thanks to the HW 2004 reviewer who pointed out the value of this example.+-- We note that the explicit type below is richer than the inferred type.+-- This richer type is needed for making this operation more polymorphic.+-- That is, a) would not work without the explicit type, while it would:+--  a)  ((+) (1::Int)) $ snd $ tuple oneTrue+--  b)  ((+) (1::Int)) $ fst $ tuple oneTrue++tuple :: ( HOccurs e1 (TIP l)+         , HType2HNat e1 l n+         , HDeleteAtHNat n l l'+         , HOccurs e2 (TIP l')+         , HOccurs e2 (TIP l)+         , HType2HNat e2 l n'+         , HDeleteAtHNat n' l l''+         , HOccurs e1 (TIP l'')+         ) =>+              TIP l -> (e1, e2)++tuple (TIP l) = let+                 x  = hOccurs (TIP l)+                 l' = hDeleteAtProxy (toProxy x) l+                 y  = hOccurs (TIP l')+                in (x,y)+++-- A specific tuple+oneTrue :: TIP (HCons Int (HCons Bool HNil))+oneTrue = hExtend (1::Int) (hExtend True emptyTIP)+++{-----------------------------------------------------------------------------}
+ Data/HList/TypeCastGeneric1.hs view
@@ -0,0 +1,22 @@+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses #-}++{-+   The HList library++   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke++   A generic implementation of type cast. For this implementation to+   work, we need to import it at a higher level in the module hierarchy+   than all clients of the class. Otherwise, type simplification will+   inline TypeCast x y, which implies compile-time unification of x and y.++   This technique works fine for ghc, and within limits for hugs.+-}++module Data.HList.TypeCastGeneric1 where++import Data.HList.FakePrelude++instance TypeCast x x+ where+  typeCast = id
+ Data/HList/TypeEqBoolGeneric.hs view
@@ -0,0 +1,16 @@+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, FlexibleContexts #-}+{-+   The HList library++   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke++   Generic implementations of type equality and disequality+-}++module Data.HList.TypeEqBoolGeneric where++import Data.HList.FakePrelude++instance            TypeEqTrue  x x+instance Fail () => TypeEqFalse x x+instance            TypeEqFalse x y
+ Data/HList/TypeEqGeneric1.hs view
@@ -0,0 +1,36 @@+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances,+  FlexibleContexts, UndecidableInstances #-}+{-+   The HList library++   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke++   A generic implementation of a type equality predicate. The given+   implementation only works for GHC. It relies on two properties+   of GHC instance selection: (i) selection is lazy, and the negation+   of the constraints of the more specific instance is assumed for+   the more general instance.++   The specific encoding given here makes use of TypeCast,+   and by transitive closure therefore relies on separate compilation+   of TypeCast clients and the TypeCast instance.++   There is another encoding in TypeEqGeneric2.hs.+-}++module Data.HList.TypeEqGeneric1 where++import Data.HList.FakePrelude++instance TypeEq x x HTrue+instance (HBool b, TypeCast HFalse b) => TypeEq x y b+-- instance TypeEq x y HFalse -- would violate functional dependency+++class HBool b => TupleType t b | t -> b+instance TupleType () HTrue+instance TupleType (x,y) HTrue+instance TupleType (x,y,z) HTrue+-- Continue for a while+instance (HBool b, TypeCast HFalse b) => TupleType x b+-- instance TupleType x HFalse -- would violate functional dependency
+ Data/HList/Variant.hs view
@@ -0,0 +1,98 @@+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances,+  UndecidableInstances, FlexibleContexts #-}++{-+   The HList library++   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke++   Variants, i.e., labelled sums.++   One approach to their implementation would be to consider both+   the favoured label and the corresponding value as dynamics upon+   variant construction. Since we are too lazy to programme some+   Typeable instances for non-ghc systems (NB: in GHC, Typeable+   is derivable), we rather model variants as (opaque) records+   with maybies for the values. Only one value will actually hold+   non-Nothing, as guaranteed by the constructor.++   See VariantP.hs for a different approach to open sums.+-}++module Data.HList.Variant where++import Data.HList.FakePrelude+import Data.HList.HListPrelude+import Data.HList.HArray+import Data.HList.Record+++{-----------------------------------------------------------------------------}++-- Variant types on the basis of label-maybe pairs.++newtype Variant mr = Variant mr+++{-----------------------------------------------------------------------------}++-- Turn proxy sequence into sequence of Nothings++class HMaybied r r' | r -> r'+ where+  hMaybied :: r -> r'++instance HMaybied HNil HNil+ where+  hMaybied _ = HNil++instance HMaybied r r'+      => HMaybied (HCons (LVPair l (Proxy v)) r) (HCons (LVPair l (Maybe v)) r')+ where+  hMaybied (HCons _ r) = HCons (LVPair Nothing) (hMaybied r)+++{-----------------------------------------------------------------------------}++-- Public constructor++mkVariant :: ( RecordLabels v ls+             , HFind x ls n+             , HMaybied v v'+             , HUpdateAtHNat n (LVPair x (Maybe y)) v' v'+             )+          => x -> y -> (Record v) -> Variant v'++mkVariant x y (Record v) = Variant v'+ where+  n       = hFind x (recordLabels v)+  ms      = hMaybied v+  v'      = hUpdateAtHNat n (newLVPair x (Just y)) ms+++{-----------------------------------------------------------------------------}++-- Public destructor++unVariant :: ( RecordLabels v ls+             , HFind x ls n+             , HLookupByHNat n v (LVPair x (Maybe y))+             )+          => x -> Variant v -> Maybe y++unVariant x (Variant v) = y+ where+  n       = hFind x (recordLabels v)+  LVPair y     = hLookupByHNat n v+++{-----------------------------------------------------------------------------}++-- Variants are opaque++instance Show (Variant v)+ where+  show _ = "<Cannot show Variant content!>"+++{-----------------------------------------------------------------------------}
+ HList.cabal view
@@ -0,0 +1,26 @@+Name:                HList+Version:             0.1+Category:            Data+Synopsis:            Heterogeneous lists+Description:         HList is a record system providing strongly typed heterogenous lists, records,+                     type-indexed products (TIP) and co-products; licensed under the MIT X License.+License:             OtherLicense+License-File:        LICENSE+Author:              2004 Oleg Kiselyov (FNMOC, Monterey), Ralf Laemmel (CWI/VU, Amsterdam),+                     Keean Schupke (Imperial College, London)+Maintainer:          oleg@pobox.com++Tested-With:         GHC==6.8.2+Build-Depends:       base+Build-Type:          Simple+Exposed-modules:     Data.HList+Other-modules:       Data.HList.Label4, Data.HList.CommonMain, Data.HList.Variant, Data.HList.GhcSyntax,+                     Data.HList.GhcRecord, Data.HList.Record, Data.HList.HZip, Data.HList.TIC, Data.HList.TIP,+                     Data.HList.HTypeIndexed, Data.HList.HOccurs, Data.HList.HArray, Data.HList.GhcExperiments,+                     Data.HList.HListPrelude, Data.HList.TypeEqBoolGeneric, Data.HList.TypeEqGeneric1,+                     Data.HList.TypeCastGeneric1, Data.HList.FakePrelude++extensions:          EmptyDataDecls, FlexibleContexts, FlexibleInstances, FunctionalDependencies,+                     MultiParamTypeClasses, OverlappingInstances, PatternSignatures, RankNTypes,+                     ScopedTypeVariables, TypeSynonymInstances, UndecidableInstances+ghc-options:         -O2 -Wall
+ LICENSE view
@@ -0,0 +1,20 @@+Copyright (c) 2004 Oleg Kiselyov (FNMOC, Monterey), Ralf Laemmel (CWI/VU, Amsterdam), Keean Schupke (Imperial College, London)++Permission is hereby granted, free of charge, to any person obtaining+a copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be+included in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE+LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION+OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION+WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ Setup.hs view
@@ -0,0 +1,3 @@+#!/usr/bin/env runhaskell+import Distribution.Simple+main = defaultMainWithHooks defaultUserHooks