poly-rec 0.7.0.2 → 0.7.0.4
raw patch · 7 files changed
+601/−50 lines, 7 filesdep ~basedep ~requirements
Dependency ranges changed: base, requirements
Files
- poly-rec.cabal +10/−9
- src/Data/GenRec.hs +274/−5
- src/Data/GenRec/Label.hs +0/−29
- src/Data/GenRec/RecInstances/Record.hs +51/−7
- src/Data/GenRec/Unordered.hs +121/−0
- src/Data/HList.hs +114/−0
- src/Data/Label.hs +31/−0
poly-rec.cabal view
@@ -1,8 +1,8 @@--- Initial polykheXrec.cabal generated by cabal init. For further+-- Initial polyrec.cabal generated by cabal init. For further -- documentation, see http://haskell.org/cabal/users-guide/ name: poly-rec-version: 0.7.0.2+version: 0.7.0.4 synopsis: Polykinded extensible records description: Extensible records/row polymorphism for Haskell. Fields are polykinded, to statically check rich structures. This library was initially conceived@@ -11,20 +11,21 @@ license-file: LICENSE author: Juan García-Garland maintainer: jpgarcia@fing.edu.uy-copyright: 2020-2022, Juan García-Garland, Marcos Viera, Alberto Pardo-category: Data+copyright: 2020-2023, Juan García-Garland, Marcos Viera, Alberto Pardo+category: Data, Dependent Types build-type: Simple extra-source-files: CHANGELOG.md cabal-version: >=1.10 library exposed-modules: Data.GenRec,- Data.GenRec.Label,- Data.GenRec.RecInstances.Record- + Data.Label,+ Data.GenRec.RecInstances.Record,+ Data.HList,+ Data.GenRec.Unordered -- other-modules: -- other-extensions:- build-depends: requirements >= 0.7.0.2 && < 0.7.1,- base >=4.11 && <4.18+ build-depends: requirements >= 0.7.0.3 && < 0.7.1,+ base >= 4.20 && < 4.21 hs-source-dirs: src default-language: Haskell2010
src/Data/GenRec.hs view
@@ -73,7 +73,8 @@ InstanceSigs, AllowAmbiguousTypes, TypeApplications,- PatternSynonyms+ PatternSynonyms,+ TypeFamilyDependencies #-} module Data.GenRec@@ -86,7 +87,10 @@ (.=.), (#), (.*.),-+ (.//),+ (↑),+ (⋉),+ (.:><), OrdType, Cmp, ShowRec,@@ -98,17 +102,26 @@ OpExtend(OpExtend), -- extend, TODO OpUpdate(OpUpdate),+ OpLJoin(OpLJoin),+ OpLeftProj(OpLeftProj), update, emptyGenRec,- module Data.GenRec.Label+ module Data.Label,++ prCmp, CmpVal,++ LabelsOf ) where import Data.Kind import Data.Proxy-import Data.GenRec.Label+import Data.Label import Data.Type.Require import Data.Type.Bool+import Data.Type.Equality ((:~:)(Refl))+import Unsafe.Coerce + import Prelude hiding (lookup) import GHC.TypeLits@@ -264,7 +277,7 @@ req ctx (OpLookup' Proxy l (ConsRec _ r)) = () -- | Pretty lookup-(#) :: forall c l r ctx v. RequireR (OpLookupCall c l r) ctx v =>+(#) :: forall c l r ctx v. RequireR (OpLookupCall c l r) v ctx => Rec c r -> Label l -> v r # l = req (Proxy @ctx) (OpLookupCall l r) @@ -452,3 +465,259 @@ ReqR (OpLookup c l r) req ctx (OpLookupCall l r) = req (Proxy @(ShowType r ': ctx)) (OpLookup l r)++++-- | HasLabel++type family Or (b :: Bool)(b' :: Bool) :: Bool where+ Or False False = False+ Or _ _ = True ++type family HasLabel (l :: k) (r :: [(k,k')]) :: Bool where+ HasLabel l '[] = False+ HasLabel l ( '(l', v) ': r) = Or (l == l') (HasLabel l r) ++-- | Left projection++data OpLeftProj+ (c :: Type)+ (ls :: [k])+ (r :: [(k, k')]) :: Type where+ OpLeftProj :: Label ls -> Rec c r -> OpLeftProj c ls r++data OpLeftProj'+ (b :: Bool) -- label in front+ (c :: Type)+ (ls:: [k])+ (r :: [(k, k')]) :: Type where+ OpLeftProj' :: Proxy b -> Label ls -> Rec c r -> OpLeftProj' b c ls r++instance+ (Require (OpLeftProj c (l ': ls :: [k]) ('[] :: [(k,k')])) ctx+ ) where+ type ReqR (OpLeftProj c (l ': ls :: [k]) ('[] :: [(k,k')]))+ = Rec c ('[] :: [(k,k')])+ req ctx _ = EmptyRec++instance+ (Require (OpLeftProj c ('[] :: [k]) (r :: [(k,k')])) ctx+ ) where+ type ReqR (OpLeftProj c ('[] :: [k]) (r :: [(k,k')]))+ = Rec c ('[] :: [(k,k')])+ req ctx _ = EmptyRec++type family InFront (l :: k) (ls::[k]) :: Bool where+ InFront l (l ': r) = True+ InFront _ _ = False++instance+ ( Require (OpLeftProj' (InFront l' (l ': ls)) c+ ((l ': ls) :: [k]) ( '(l',v) ': r)) ctx+ , ReqR (OpLeftProj c (l ': ls) ('(l', v) : r))+ ~ ReqR (OpLeftProj' (InFront l' (l ': ls)) c (l ': ls) ('(l', v) : r))+ )+ => Require (OpLeftProj c ((l ': ls) :: [k]) ( '(l',v) ': r)) ctx where+ type ReqR (OpLeftProj c ((l ': ls) :: [k]) ( '(l',v) ': r))+ = ReqR (OpLeftProj' (InFront l' (l ': ls)) c+ ((l ': ls) :: [k]) ('(l',v) ': r))+ req ctx (OpLeftProj pls r) =+ let pr = Proxy @(InFront l' (l ': ls))+ in req ctx (OpLeftProj' pr pls r)+++type family LabelsOf (r :: [(k, k')]) :: [k] where+ LabelsOf '[] = '[]+ LabelsOf ( '(l, v) ': r) = l ': LabelsOf r++instance+ ( ReqR (OpLeftProj c (ls :: [k]) (r :: [(k,k')]))+ ~ Rec c (UnWrap @k @k' (ReqR (OpLeftProj c ls r)))+ , Require (OpLeftProj c ls r) ctx)+ => Require (OpLeftProj' 'True c (l ': ls) ( '(l,v) ': r)) ctx where+ type ReqR (OpLeftProj' 'True c (l ': ls) ( '(l,v) ': r))+ = Rec c ('(l,v) ': UnWrap (ReqR (OpLeftProj c ls r)))+ req ctx (OpLeftProj' _ pls (ConsRec lv r))+ = ConsRec lv $ req ctx (OpLeftProj (Label @ls) r)++instance+ (Require (OpLeftProj c (l ': ls) r) ctx)+ => Require (OpLeftProj' 'False c (l ': ls) ( '(l',v) ': r)) ctx where+ type ReqR (OpLeftProj' 'False c (l ': ls) ( '(l',v) ': r))+ = ReqR (OpLeftProj c (l ': ls) r)+ req ctx (OpLeftProj' _ ls (ConsRec _ r)) = req ctx (OpLeftProj ls r)++instance+ Require (OpLeftProj' 'False c (l ': ls) ('[] :: [(k,k')]) ) ctx where+ type ReqR (OpLeftProj' 'False c (l ': ls) ('[] :: [(k,k')]))+ = Rec c ('[] :: [(k, k')])+ req ctx _ = EmptyRec++infixr 5 .//+ls .// r = req emptyCtx (OpLeftProj ls r)+++-- | extend or update++data OpExtUpd (c :: Type)+ (l :: k)+ (v :: k')+ (r :: [(k, k')]) :: Type where+ OpExtUpd :: Label l -> WrapField c v -> Rec c r+ -> OpExtUpd c l v r++data OpExtUpd' (b :: Ordering)+ (c :: Type)+ (l :: k)+ (v :: k')+ (r :: [(k, k')]) :: Type where+ OpExtUpd' :: Proxy b -> Label l -> WrapField c v -> Rec c r+ -> OpExtUpd' b c l v r++instance Require (OpExtUpd c l v '[]) ctx where+ type ReqR (OpExtUpd c l v '[]) = Rec c '[ '(l,v)]+ req ctx (OpExtUpd lv vv EmptyRec) = lv .=. vv .*. EmptyRec++instance+ Require (OpExtUpd' (Cmp l l₁) c l v ( '(l₁,v₁) ': r)) ctx+ => Require (OpExtUpd c l v ( '(l₁,v₁) ': r)) ctx where+ type ReqR (OpExtUpd c l v ( '(l₁,v₁) ': r))+ = ReqR (OpExtUpd' (Cmp l l₁) c l v ( '(l₁,v₁) ': r))+ req ctx (OpExtUpd lv vv r)+ = req ctx (OpExtUpd' @(Cmp l l₁) @_ @_ @v+ Proxy lv vv r)+ +instance Require (OpExtUpd' 'EQ c l v ( '(l, v₁) ': r)) ctx where+ type ReqR (OpExtUpd' 'EQ c l v ( '(l, v₁) ': r))+ = Rec c ( '(l, v) ': r)+ req ctx (OpExtUpd' _ lv vv (ConsRec _ r))+ = ConsRec @_ @_ @v (lv .=. vv) r++instance Require (OpExtUpd' 'LT c l v ( '(l₁, v₁) ': r)) ctx where+ type ReqR (OpExtUpd' 'LT c l v ( '(l₁, v₁) ': r))+ = Rec c ( '(l, v) ': '(l₁, v₁) ': r)+ req ctx (OpExtUpd' _ lv vv r) = (lv .=. vv) `ConsRec` r++instance+ (Require (OpExtUpd c (l :: k) (v :: k') r) ctx,+ ReqR (OpExtUpd c l v r)+ ~ Rec c (UnWrap @k @k' (ReqR (OpExtUpd c l v r))))+ =>+ Require (OpExtUpd' 'GT c l v ( '(l₁, v₁) ': r)) ctx where+ type ReqR (OpExtUpd' 'GT c l v ( '(l₁, v₁) ': r)) =+ Rec c ( '(l₁, v₁) ': UnWrap (ReqR (OpExtUpd c l v r)))+ req ctx (OpExtUpd' _ lv vv (ConsRec lv₁ r)) =+ lv₁ `ConsRec` (req ctx (OpExtUpd @_ @_ @v lv vv r))+++r ↑ (TagField _ _ v :: TagField c l v)+ = req emptyCtx (OpExtUpd (Label @l) v r)++-- | Left join++type family LJoin (rₗ :: [(k,k')]) (rᵣ :: [(k,k')]) :: [(k,k')] where+ LJoin '[] rᵣ = rᵣ+ LJoin rₗ '[] = rₗ+ LJoin ( '(lₗ,vₗ) ': rₗ) ( '(lᵣ,vᵣ) ': rᵣ)+ = If (Cmp lₗ lᵣ == 'LT)+ ( '(lₗ,vₗ) ': LJoin rₗ ( '(lᵣ,vᵣ) ': rᵣ))+ (If (Cmp lₗ lᵣ == 'EQ)+ ( '(lₗ,vₗ) ': LJoin rₗ rᵣ)+ ( '(lᵣ,vᵣ) ': LJoin ( '(lₗ,vₗ) ': rₗ) rᵣ))++data OpLJoin (c :: Type)+ (rₗ :: [(k,k')])+ (rᵣ :: [(k,k')]) :: Type where+ OpLJoin :: Rec c rₗ -> Rec c rᵣ -> OpLJoin c rₗ rᵣ++instance Require (OpLJoin c '[] rᵣ) ctx where+ type ReqR (OpLJoin c '[] rᵣ) = Rec c rᵣ+ req ctx (OpLJoin _ r) = r++instance Require (OpLJoin c (x ': r_l) '[]) ctx where+ type ReqR (OpLJoin c (x ': r_l) '[]) = Rec c (x ': r_l)+ req ctx (OpLJoin r _) = r++data OpLJoin' (b :: Ordering)+ (c :: Type)+ (rₗ :: [(k,k')])+ (rᵣ :: [(k,k')]) :: Type where+ OpLJoin' :: Proxy b -> Rec c rₗ -> Rec c rᵣ -> OpLJoin' b c rₗ rᵣ++instance (+ Require (OpLJoin' (Cmp lₗ lᵣ) c ( '(lₗ, vₗ) ': rₗ) ( '(lᵣ, vᵣ) ': rᵣ)) ctx+ )+ => Require (OpLJoin c ( '(lₗ, vₗ) ': rₗ) ( '(lᵣ, vᵣ) ': rᵣ)) ctx where+ type ReqR (OpLJoin c ( '(lₗ, vₗ) ': rₗ) ( '(lᵣ, vᵣ) ': rᵣ))+ = ReqR (OpLJoin' (Cmp lₗ lᵣ) c ( '(lₗ, vₗ) ': rₗ) ( '(lᵣ, vᵣ) ': rᵣ))+ req ctx (OpLJoin (ConsRec lvₗ rₗ) (ConsRec lvᵣ rᵣ))+ = req ctx (OpLJoin' (Proxy @(Cmp lₗ lᵣ))+ (ConsRec lvₗ rₗ) (ConsRec lvᵣ rᵣ))++instance+ (Require (OpLJoin c rₗ ( '(lᵣ,vᵣ) ': (rᵣ :: [(k,k')]))) ctx+ , ReqR (OpLJoin c rₗ ('(lᵣ, vᵣ) : rᵣ))+ ~ Rec c (UnWrap @k @k'(ReqR (OpLJoin c rₗ ('(lᵣ, vᵣ) : rᵣ)))))+ =>+ Require (OpLJoin' 'LT c ( '(lₗ, vₗ) ': rₗ) ( '(lᵣ, vᵣ) ': rᵣ)) ctx where+ type ReqR (OpLJoin' 'LT c ( '(lₗ, vₗ) ': rₗ) ( '(lᵣ, vᵣ) ': rᵣ))+ = Rec c ('(lₗ,vₗ) ': UnWrap (ReqR (OpLJoin c rₗ ( '(lᵣ,vᵣ) ': rᵣ))))+ req ctx (OpLJoin' _ (ConsRec lvₗ rₗ) (ConsRec lvᵣ rᵣ))+ = lvₗ `ConsRec` (req ctx (OpLJoin rₗ (ConsRec lvᵣ rᵣ)))++instance+ (Require (OpLJoin c ('(lₗ, vₗ) : rₗ) (rᵣ :: [(k,k')])) ctx+ , ReqR (OpLJoin c ('(lₗ, vₗ) : rₗ) rᵣ)+ ~ Rec c (UnWrap @k @k' (ReqR (OpLJoin c ('(lₗ, vₗ) : rₗ) rᵣ)))+ )+ =>+ Require (OpLJoin' 'GT c ( '(lₗ, vₗ) ': rₗ) ( '(lᵣ, vᵣ) ': rᵣ)) ctx where+ type ReqR (OpLJoin' 'GT c ( '(lₗ, vₗ) ': rₗ) ( '(lᵣ, vᵣ) ': rᵣ))+ = Rec c ('(lᵣ,vᵣ) ': UnWrap (ReqR (OpLJoin c ( '(lₗ,vₗ) ': rₗ) rᵣ)))+ req ctx (OpLJoin' _ (ConsRec lvₗ rₗ) (ConsRec lvᵣ rᵣ))+ = lvᵣ `ConsRec` (req ctx (OpLJoin (ConsRec lvₗ rₗ) rᵣ))++instance+ (ReqR (OpLJoin c rₗ (rᵣ :: [(k,k')]))+ ~ Rec c (UnWrap @k @k' (ReqR (OpLJoin c rₗ rᵣ))),+ Require (OpLJoin c rₗ rᵣ) ctx)+ => Require (OpLJoin' 'EQ c ( '(l, vₗ) ': rₗ) ( '(l, vᵣ) ': rᵣ)) ctx where+ type ReqR (OpLJoin' 'EQ c ( '(l, vₗ) ': rₗ) ( '(l, vᵣ) ': rᵣ))+ = Rec c ( '(l, vₗ) ': UnWrap (ReqR (OpLJoin c rₗ rᵣ)))+ req ctx (OpLJoin' _ (ConsRec lvₗ rₗ) (ConsRec _ rᵣ))+ = lvₗ `ConsRec` (req ctx (OpLJoin rₗ rᵣ))++++(⋉) :: Require (OpLJoin c rₗ rᵣ) '[] =>+ Rec c rₗ+ -> Rec c rᵣ -> ReqR (OpLJoin c rₗ rᵣ)+rₗ ⋉ rᵣ = req emptyCtx (OpLJoin rₗ rᵣ)+rₗ .:>< rᵣ = req emptyCtx (OpLJoin rₗ rᵣ)++data SComp (b :: Ordering) where+ SEQ :: SComp 'EQ+ SLT :: SComp 'LT+ SGT :: SComp 'GT++-- term-level comparison+class CmpVal (l :: k)(l₁ :: k) where+ cmpVal :: Label l -> Label l₁ -> Ordering++instance (KnownSymbol l, KnownSymbol l₁) + => CmpVal (l :: Symbol) (l₁ :: Symbol) where+ cmpVal l r = compare (symbolVal l)(symbolVal r)++prCmp :: CmpVal lₗ lᵣ =>+ (TagField c lₗ vₗ) -> (TagField c lᵣ vᵣ)+ -> SComp (Cmp lₗ lᵣ)+prCmp (_ :: TagField c lₗ vₗ)+ (_ :: TagField c lᵣ vᵣ)+ = case cmpVal (Label @lₗ) (Label @lᵣ) of+ LT -> case unsafeCoerce Refl :: Cmp lₗ lᵣ :~: 'LT of+ Refl -> SLT+ GT -> case unsafeCoerce Refl :: Cmp lₗ lᵣ :~: 'GT of+ Refl -> SGT+ EQ -> case unsafeCoerce Refl :: Cmp lₗ lᵣ :~: 'EQ of+ Refl -> SEQ+
− src/Data/GenRec/Label.hs
@@ -1,29 +0,0 @@-{-|-Module : Language.Grammars.AspectAG.Label-Description : Labels (polykinded, phantom)-Copyright : (c) Juan García Garland, Marcos Viera 2020-License : GPL-3-Maintainer : jpgarcia@fing.edu.uy-Stability : experimental-Portability : POSIX--}--{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE DataKinds #-}--module Data.GenRec.Label where-import Data.Proxy--data Label l = Label--sndLabel :: Label '(a,b) -> Label b-sndLabel _ = undefined--fstLabel :: Label '(a,b) -> Label a-fstLabel _ = undefined--labelFromType :: a -> Label a-labelFromType _ = Label--proxyToLabel :: Proxy a -> Label a-proxyToLabel _ = Label
src/Data/GenRec/RecInstances/Record.hs view
@@ -23,7 +23,7 @@ (Record, Reco, untag, getLabel, (.==.), (.**.), (##),- emptyRecord+ emptyRecord, Tagged (..), Tagged ) where @@ -31,9 +31,12 @@ import Data.Kind import Data.Proxy import Data.GenRec-import Data.GenRec.Label+import Data.Label +import Data.Type.Equality+import Unsafe.Coerce + -- | * Records -- | datatype definition@@ -112,11 +115,6 @@ in '{' : show lv ++ ", " ++ shr -r = (Label @"integer" .==. (3 :: Integer))- .**. (Label @"boolean" .==. True)- .**. emptyRecord-- data Mat type Matrix = Rec Mat :: [(Nat, [(Symbol, Type)])] -> Type @@ -148,3 +146,49 @@ -- m' = TagField @Mat (Label @Mat) (Label @1) r -- .*. TagField (Label @Mat) (Label @2) (EmptyRec :: Record ('[] :: [(Symbol, Type)])) -- .*. EmptyRec++rCast :: Record '[ '("int", Int)]+rCast = castWith (sym bad) r+ where bad :: Record '[ '("int", Int)]+ :~: Record '[ '("boolean", Bool), '("int", Int)]+ bad = unsafeCoerce Refl -- undefined no funciona porque se evalúa la prueba+++r = (Label @"int" .==. (3 :: Int))+ .**. (Label @"boolean" .==. True)+ .**. emptyRecord+++-- r1 :: Record+-- '[ '("boolean", Bool),+-- '("boolean2", Bool),+-- '("int", Int),+-- '("int2", Int)]+r1 = (Label @"int" .==. (3 :: Int))+ .**. (Label @"boolean" .==. True)+ .**. (Label @"int2" .==. (5 :: Int))+ .**. (Label @"boolean2" .==. False)+ .**. emptyRecord++-- r2 :: Record+-- '[ '("char", Char),+-- '("int", Int),+-- '("integer", Integer),+-- '("unit", ())]+r2 = (Label @"int" .==. (40 :: Int))+ .**. (Label @"unit" .==. ())+ .**. (Label @"integer" .==. (5 :: Integer))+ .**. (Label @"boolean" .==. False)+ .**. emptyRecord++t3 = r1 # Label @"int"+tTrue = r1 # Label @"boolean"++r12 = r1 .:>< r2++-- r12 == {boolean : True,+-- boolean2 : False,+-- int : 3,+-- int2 : 5,+-- integer : 5,+-- unit : ()}
+ src/Data/GenRec/Unordered.hs view
@@ -0,0 +1,121 @@+{-|+Module : Data.GenRecord.Unordered+Description : polykinded extensible record library+Copyright : (c) Juan García Garland (2023)+License : GPL+Maintainer : jpgarcia@fing.edu.uy+Stability : experimental+Portability : POSIX++Records where labels are names (|Symbol|s) and preserve the insertion+order (hence they are not ordered alphanumerically).++We did not reuse Generic record constructs from |Data.GenRec| and+built new definitions instead. This module is intended to mimmick+ordinary Haskell records, while being extensive.++One quirk of the definitions in this module is that we admit repeated+labels. Ordinary lookup will get the first occurrence, but we build+different kind of projections to get all values under a label. This+development was first intended to represent a collection of registers+with names and values, hence the field name.++-}++{-# OPTIONS_GHC -fno-warn-missing-methods #-}++{-# LANGUAGE DataKinds,+ TypeOperators,+ PolyKinds,+ GADTs,+ RankNTypes,+ StandaloneDeriving,+ FlexibleInstances,+ FlexibleContexts,+ ConstraintKinds,+ MultiParamTypeClasses,+ FunctionalDependencies,+ UndecidableInstances,+ ScopedTypeVariables,+ TypeFamilies,+ InstanceSigs,+ AllowAmbiguousTypes,+ TypeApplications,+ PatternSynonyms,+ DataKinds, PolyKinds+#-}++module Data.GenRec.Unordered where+import Data.Label+import GHC.TypeLits (Symbol, symbolVal, KnownSymbol)+import Data.Kind+import Data.Proxy+import Data.Type.Require++import Data.GenRec (UnWrap)++data Reg (l :: Symbol) v where+ Reg :: (KnownSymbol l) => v -> Reg l v++instance+ Show v+ =>+ Show (Reg l v) where+ show (Reg v) = symbolVal (Proxy @l) ++ " : " ++ show v++infixr 5 :<+data Record (r :: [(Symbol, Type)]) :: Type where+ Empty :: Record '[] -- ^ empty record+ (:<) :: Reg l v -> Record r -> Record ('( l, v) ': r) -- ^++instance+ Show (Record '[]) where+ show Empty = "{}"++instance+ (Show v)+ =>+ Show (Record '[ '(l,v)]) where+ show (reg :< _) = "{ " ++ show reg ++ "}"+ +instance+ ( Show v+ , Show (Record (lv ': r)))+ =>+ Show (Record ( '(l, v) ': lv ': r)) where+ show (reg :< r) = "{" ++ show reg ++ ", " ++ tail (show r)++ex1 = Reg @"x" 3.0+ :< Reg @"y" 2.1+ :< Reg @"z" ()+ :< Reg @"t" 0+ :< Empty++ex2 = Reg @"header" ()+ :< Reg @"val" 2.1+ :< Reg @"val" 1.1+ :< Reg @"val" 0.0+ :< Reg @"footer" "END"+ :< Empty++type instance UnWrap (Record l) = l++data OpSnoc (l :: Symbol) (v :: Type) (r :: [(Symbol, Type)]) where+ OpSnoc :: Reg l v -> Record r -> OpSnoc l v r++instance+ Require (OpSnoc l v '[]) ctx where+ type ReqR (OpSnoc l v '[])+ = Record '[ '(l, v)]+ req ctx (OpSnoc lv _) = lv :< Empty+++instance+ RequireR (OpSnoc l v r) (Record (UnWrap (ReqR (OpSnoc l v r)))) ctx+ =>+ Require (OpSnoc l v ( '(l',v') ': r)) ctx where+ type ReqR (OpSnoc l v ( '(l',v') ': r)) =+ Record ( '(l',v') ': UnWrap @Symbol @Type (ReqR (OpSnoc l v r)))+ req ctx (OpSnoc lv (lv' :< r)) = lv' :< req ctx (OpSnoc lv r) ++r >: lv = req (Proxy @'[]) (OpSnoc lv r)
+ src/Data/HList.hs view
@@ -0,0 +1,114 @@+{-|+Module : Data.HList+Description :+Implementation of strongly typed heterogeneous lists.+Copyright : (c) Juan García Garland, 2018,2023+License : GPL+Maintainer : jpgarcia@fing.edu.uy+Stability : experimental+Portability : POSIX+|-}++{-# OPTIONS_GHC -fno-warn-missing-methods,+ -fno-warn-partial-type-signatures #-}++{-# LANGUAGE DataKinds,+ TypeOperators,+ PolyKinds,+ GADTs,+ TypeInType,+ RankNTypes,+ StandaloneDeriving,+ FlexibleInstances,+ FlexibleContexts,+ ConstraintKinds,+ MultiParamTypeClasses,+ FunctionalDependencies,+ UndecidableInstances,+ ScopedTypeVariables,+ TypeFamilies,+ InstanceSigs,+ AllowAmbiguousTypes,+ TypeApplications,+ PatternSynonyms,+ PartialTypeSignatures+#-}++module Data.HList where++import Data.Kind+import Data.Proxy+import Data.Label+import Data.Type.Bool+import Data.Type.Equality++-- |Heterogeneous lists are implemented as a GADT+data HList (l :: [Type]) :: Type where+ HNil :: HList '[]+ HCons :: x -> HList xs -> HList (x ': xs)++hHead :: HList (t ': _) -> t+hHead (HCons v _) = v+++-- | HMember is a test membership function.+--Since we are in Haskell the value level function computes with the evidence +class HMember (t :: Type) (l :: [Type]) where+ type HMemberRes t l :: Bool+ hMember :: Label t -> HList l -> Proxy (HMemberRes t l)++instance HMember t '[] where+ type HMemberRes t '[] = 'False+ hMember _ _ = Proxy++instance HMember t (t' ': ts) where+ type HMemberRes t (t' ': ts) = t == t' || HMemberRes t ts+ hMember _ _ = Proxy++-- | HMember' is a test membership function.+-- But looking up in a list of Labels+class HMember' (t :: k) (l :: [k]) where+ type HMemberRes' t l :: Bool+ hMember' :: f t -> LList l -> Proxy (HMemberRes' t l)++instance HMember' t '[] where+ type HMemberRes' t '[] = 'False+ hMember' _ _ = Proxy++instance HMember' t (t' ': ts) where+ type HMemberRes' t (t' ': ts) = t == t' || HMemberRes' t ts+ hMember' _ _ = Proxy+++-- | No other functionality is needed for AAG++infixr 2 .:+(.:) = HCons+ε = HNil+hn = HNil++-- | a polykinded heteogeneous list of labels+data LList (l :: [k]) :: Type where+ LNil :: LList '[]+ LCons :: Label h -> LList l -> LList (h ': l)++infixr 2 .:.+(.:.) = LCons+lL = LNil++lHead :: LList (t ': ts) -> Label t+lHead _ = Label++class LListFrom (l :: [k]) where+ lListFrom :: Proxy l -> LList l++instance LListFrom ('[] :: [k]) where+ lListFrom (Proxy :: Proxy '[])= LNil++instance LListFrom ts => LListFrom (t ': ts) where+ lListFrom (Proxy :: Proxy (t ': ts))+ = LCons Label $ lListFrom Proxy++type family Snoc (l :: [k]) (v :: k) where+ Snoc '[] v = '[v]+ Snoc (x ': xs) v = x ': Snoc xs v
+ src/Data/Label.hs view
@@ -0,0 +1,31 @@+{-|+Module : Data.Label+Description : Labels (polykinded, phantom).+ Basically a reimplementation of Proxy,+ where we have control over the codebase+Copyright : (c) Juan García Garland, Marcos Viera 2020+License : GPL-3+Maintainer : jpgarcia@fing.edu.uy+Stability : experimental+Portability : POSIX+-}++{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE DataKinds #-}++module Data.Label where+import Data.Proxy++data Label l = Label++sndLabel :: Label '(a,b) -> Label b+sndLabel _ = undefined++fstLabel :: Label '(a,b) -> Label a+fstLabel _ = undefined++labelFromType :: a -> Label a+labelFromType _ = Label++proxyToLabel :: Proxy a -> Label a+proxyToLabel _ = Label