diff --git a/CTRex.cabal b/CTRex.cabal new file mode 100644 --- /dev/null +++ b/CTRex.cabal @@ -0,0 +1,23 @@ +Name: CTRex +Version: 0.5 +Synopsis: Open records using closed type families. +Description: Open records using closed type families. +License: BSD3 +License-file: LICENSE +Author: Atze van der Ploeg +Maintainer: atzeus@gmail.com +Homepage: http://www.haskell.org/haskellwiki/CTRex +Build-Type: Simple +Cabal-Version: >=1.6 +Data-files: ChangeLog +Category: Data, Data Structures +Tested-With: GHC==7.8.2 +Library + Build-Depends: base >= 2 && <= 6, unordered-containers >= 0.2, hashable >= 1.2, mtl >= 1.0 + Exposed-modules: Data.OpenRecords + other-modules: + Extensions: TypeOperators, ScopedTypeVariables,GADTs, KindSignatures, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, TypeFamilies, ViewPatterns, DataKinds, ConstraintKinds, UndecidableInstances,FunctionalDependencies,RankNTypes,AllowAmbiguousTypes, InstanceSigs, PolyKinds + +source-repository head + type: git + location: https://github.com/atzeus/CTRex diff --git a/ChangeLog b/ChangeLog new file mode 100644 --- /dev/null +++ b/ChangeLog @@ -0,0 +1,1 @@ +0.5 : Initial version diff --git a/Data/OpenRecords.hs b/Data/OpenRecords.hs new file mode 100644 --- /dev/null +++ b/Data/OpenRecords.hs @@ -0,0 +1,522 @@ +{-# LANGUAGE TypeOperators, ScopedTypeVariables,GADTs, KindSignatures, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, TypeFamilies, ViewPatterns, DataKinds, ConstraintKinds, UndecidableInstances,FunctionalDependencies,RankNTypes,AllowAmbiguousTypes, InstanceSigs, PolyKinds #-} +----------------------------------------------------------------------------- +-- | +-- Module : Data.OpenRecords +-- Copyright : (c) Atze van der Ploeg 2013 +-- License : BSD-style +-- Maintainer : atzeus@gmail.org +-- Stability : expirimental +-- +-- This module implements extensible records using closed type famillies. +-- +-- See the . +-- +-- Lists of (label,type) pairs are kept sorted thereby ensuring +-- that { x = 0, y = 0 } and { y = 0, x = 0 } have the same type. +-- +-- In this way we can implement standard type classes such as Show, Eq, Ord and Bounded +-- for open records, given that all the elements of the open record satify the constraint. +-- +----------------------------------------------------------------------------- + + +module Data.OpenRecords + + ( + -- * Types and constraints + Label(..), + KnownSymbol(..), + Rec, Row, + -- * Construction + empty,Empty , + -- ** Extension + extend, extendUnique, Extend, + -- ** Renaming + rename, renameUnique, Rename, + -- ** Restriction + (.-), (:-), + -- ** Update + update, + -- * Query + (.!), (:!), + -- * Combine + -- ** Union + (.++), (:++), + -- ** Disjoint union + (.+) , (:+), + -- * Row constraints + (:\), Disjoint, Labels(..), Forall(..), CWit, FWit, + -- * Row only operations + -- * Syntactic sugar + RecOp(..), RowOp(..), (.|), (:|) + + + + + ) +where + +import Data.HashMap.Lazy(HashMap) +import Data.Sequence(Seq,viewl,ViewL(..),(><),(<|)) +import qualified Data.HashMap.Lazy as M +import qualified Data.Sequence as S +import Unsafe.Coerce +import Data.List +import GHC.TypeLits +import GHC.Exts -- needed for constraints kinds +import Data.Type.Equality (type (==)) + + +-- | A label +data Label (s :: Symbol) = Label + +instance KnownSymbol s => Show (Label s) where + show = symbolVal + + + + +{-------------------------------------------------------------------- + Row constraints +--------------------------------------------------------------------} + +-- | Does the row lack (i.e. it has not) the specified label? + +type r :\ l = (LacksP l r ~ LabelUnique l) +-- | Are the two rows disjoint? (i.e. their sets of labels are disjoint) +type Disjoint l r = (DisjointR l r ~ IsDisjoint) + + + + +-- private things for row operations + + + +{-------------------------------------------------------------------- + Open records +--------------------------------------------------------------------} + +data HideType where + HideType :: a -> HideType + +-- | A record with row r. +data Rec (r :: Row *) where + OR :: HashMap String (Seq HideType) -> Rec r + +-- | The kind of rows. This type is only used as a datakind. A row is a typelevel entity telling us +-- which symbols are associated with which types. +newtype Row a = R [LT a] -- constructor not exported + +-- | The empty record +empty :: Rec Empty +empty = OR M.empty + +-- | Type level variant of 'empty' +type family Empty :: Row * where + Empty = R '[] + +{-------------------------------------------------------------------- + Basic record operations +--------------------------------------------------------------------} + + +-- | Record extension. The row may already contain the label, +-- in which case the origin value can be obtained after restriction ('.-') with +-- the label. +extend :: KnownSymbol l => Label l -> a -> Rec r -> Rec (Extend l a r) +extend (show -> l) a (OR m) = OR $ M.insert l v m + where v = HideType a <| M.lookupDefault S.empty l m + +-- | Record extension without shadowing. The row may not already contain label l. +extendUnique :: (KnownSymbol l,r :\ l) => Label l -> a -> Rec r -> Rec (Extend l a r) +extendUnique = extend + +-- | Type level operations of 'extend' and 'extendUnique' +type family Extend (l :: Symbol) (a :: *) (r :: Row *) :: Row * where + Extend l a (R x) = R (Inject (l :-> a) x) + +-- | Update the value associated with the label. +update :: KnownSymbol l => Label l -> r :! l -> Rec r -> Rec r +update (show -> l) a (OR m) = OR $ M.adjust f l m where f = S.update 0 (HideType a) + +-- | Rename a label. The row may already contain the new label , +-- in which case the origin value can be obtained after restriction ('.-') with +-- the new label. +rename :: (KnownSymbol l, KnownSymbol l') => Label l -> Label l' -> Rec r -> Rec (Rename l l' r) +rename l l' r = extend l' (r .! l) (r .- l) + +-- | Rename a label. The row may not already contain the new label. +renameUnique :: (KnownSymbol l, KnownSymbol l', r :\ l') => Label l -> Label l' -> Rec r -> Rec (Rename l l' r) +renameUnique = rename + +-- | Type level operation of 'rename' and 'renameUnique' +type family Rename (l :: Symbol) (l' :: Symbol) (r :: Row *) :: Row * where + Rename l l' r = Extend l' (r :! l) (r :- l) + +infix 8 .- +-- | Record selection +(.!) :: KnownSymbol l => Rec r -> Label l -> r :! l +(OR m) .! (show -> a) = x' + where x S.:< t = S.viewl $ m M.! a + -- notice that this is safe because of the external type + x' = case x of HideType p -> unsafeCoerce p + + + +infixl 6 :! +-- | Type level operation of '.!' +type family (r :: Row *) :! (t :: Symbol) :: * where + (R r) :! l = Get l r + +-- | Record restriction. Delete the label l from the record. +(.-) :: KnownSymbol l => Rec r -> Label l -> Rec (r :- l) +(OR m) .- (show -> a) = OR m' + where x S.:< t = S.viewl $ m M.! a + m' = case S.viewl t of + EmptyL -> M.delete a m + _ -> M.insert a t m + +-- | Type level operation of '.-' +type family (r :: Row *) :- (s :: Symbol) :: Row * where + (R r) :- l = R (Remove l r) + + + +-- | Record union (not commutative) +(.++) :: Rec l -> Rec r -> Rec (l :++ r) +(OR l) .++ (OR r) = OR $ M.unionWith (><) l r + +-- | Type level operation of '.++' +type family (l :: Row *) :++ (r :: Row *) :: Row * where + (R l) :++ (R r) = R (Merge l r) + +-- | Record disjoint union (commutative) +(.+) :: Disjoint l r => Rec l -> Rec r -> Rec (l :+ r) +(OR l) .+ (OR r) = OR $ M.unionWith (error "Impossible") l r + +-- | Type level operation of '.+' +type family (l :: Row *) :+ (r :: Row *) :: Row * where + (R l) :+ (R r) = R (Merge l r) + +{-------------------------------------------------------------------- + Syntactic sugar for record operations +--------------------------------------------------------------------} +-- | A constraint not constraining anything +class NoConstr a +instance NoConstr a + +-- | Alias for ':\'. It is a class rather than an alias, so that +-- it can be partially appliced. +class (r :\ l) => Lacks (l :: Symbol) (r :: Row *) +instance (r :\ l) => Lacks l r + + +-- | Alias for @(r :! l) ~ a@. It is a class rather than an alias, so that +-- it can be partially appliced. +class ((r :! l) ~ a ) => HasType l a r +instance ((r :! l) ~ a ) => HasType l a r + + +infix 5 := +infix 5 :!= +infix 5 :<- + +-- | Here we provide a datatype for denoting record operations. Use '.|' to +-- actually apply the operations. +-- +-- This allows us to chain operations with nicer syntax. +-- For example we can write: +-- +-- > p :<-| z .| y :<- 'b' .| z :!= False .| x := 2 .| y := 'a' .| empty +-- +-- Which results in: +-- +-- > { p=False, x=2, y='b' } +-- +-- Without this sugar, we would have written it like this: +-- +-- > rename z p $ update y 'b' $ extendUnique z False $ extend x 2 $ extend y 'a' empty +-- +-- +-- [@:<-@] Record update. Sugar for 'update'. +-- +-- [@:=@] Record extension. Sugar for 'extend'. +-- +-- [@:!=@] Record extension, without shadowing. Sugar for 'extendUnique'. +-- +-- [@:<-|@] Record label renaming. Sugar for 'rename'. +-- +-- [@:<-!@] Record label renaming. Sugar for 'renameUnique'. +data RecOp (c :: Row * -> Constraint) (rowOp :: RowOp *) where + (:<-) :: KnownSymbol l => Label l -> a -> RecOp (HasType l a) RUp + (:=) :: KnownSymbol l => Label l -> a -> RecOp NoConstr (l ::= a) + (:!=) :: KnownSymbol l => Label l -> a -> RecOp (Lacks l) (l ::= a) + (:<-|) :: (KnownSymbol l, KnownSymbol l') => Label l' -> Label l -> RecOp NoConstr (l' ::<-| l) + (:<-!) :: (KnownSymbol l, KnownSymbol l', r :\ l') => Label l' -> Label l -> RecOp (Lacks l') (l' ::<-| l) + + + +-- | Type level datakind corresponding to 'RecOp'. +-- Here we provide a datatype for denoting row operations. Use ':|' to +-- actually apply the type level operation. +-- +-- This allows us to chain type level operations with nicer syntax. +-- For example we can write: +-- +-- > "p" ::<-| "z" :| RUp :| "z" ::= Bool :| "x" ::= Double :| "y" ::= Char :| Empty +-- +-- As the type of the expression: +-- +-- > p :<-| z .| y :<- 'b' .| z :!= False .| x := 2 .| y := 'a' .| empty +-- +-- Without this sugar, we would have written it like this: +-- +-- > Rename "p" "z" (Extend "z" Bool (Extend x Double (Extend "x" Int Empty))) +-- +-- Of course, we can also just write: +-- +-- > "p" ::= Bool :| "x" ::= Double :| "y" ::= Int :| Empty +-- +-- instead, doing the computation ourselves, or even let the type infer. +-- +-- [@RUp@] Type level equivalent of ':<-'. Is the identity Row Operation. +-- +-- [@::=@] Type level equivalent of ':='. Row extension. Sugar for 'Extend'. +-- +-- [@::<-|@] Type level equivalent of ':<-|'. Row label renaming. Sugar for 'Rename'. + + +infix 5 ::= +infix 5 ::<-| +data RowOp (a :: *) where + RUp :: RowOp a + (::=) :: Symbol -> a -> RowOp a + (::<-|) :: Symbol -> Symbol -> RowOp a + +-- | Apply an operation to a record. +infixr 4 .| +(.|) :: c r => RecOp c ro -> Rec r -> Rec (ro :| r) +(l :<- a) .| m = update l a m +(l := a) .| m = extend l a m +(l :!= a) .| m = extendUnique l a m +(l' :<-| l) .| m = rename l l' m +(l' :<-! l) .| m = renameUnique l l' m + +-- | Apply a (typelevel) operation to a row. Type level operation of '.|' +infixr 4 :| +type family (x :: RowOp *) :| (r :: Row *) :: Row * where + RUp :| r = r + (l ::= a) :| r = Extend l a r + (l' ::<-| l) :| r = Rename l l' r + +{-------------------------------------------------------------------- + Constrained record operations +--------------------------------------------------------------------} + + + +class Labels (r :: Row *) where + labels :: Rec r -> [String] + +instance Labels (R '[]) where + labels _ = [] + +instance (KnownSymbol l , Labels (R t)) => Labels (R (l :-> v ': t)) where + labels r = show l : labels (r .- l) where l = Label :: Label l + +-- | A witness of a constraint. For use like this @rinit (CWit :: CWit Bounded) minBound@ +data CWit (c :: * -> Constraint) = CWit + + +-- | If the constaint @c@ holds for all elements in the row @r@, +-- then the methods in this class are available. +class Forall (r :: Row *) (c :: * -> Constraint) where + -- | Given a default value @a@, where@a@ can be instantiated to each type in the row, + -- create a new record in which all elements carry this default value. + rinit :: CWit c -> (forall a. c a => a) -> Rec r + -- | Given a function @(a -> b)@ where @a@ can be instantiated to each type in the row, + -- apply the function to each element in the record and collect the result in a list. + + erase :: CWit c -> (forall a. c a => a -> b) -> Rec r -> [b] + -- | Given a function @(a -> a -> b)@ where @a@ can be instantiated to each type of the row, + -- apply the function to each pair of values that can be obtained by indexing the two records + -- with the same label and collect the result in a list. + eraseZip :: CWit c -> (forall a. c a => a -> a -> b) -> Rec r -> Rec r -> [b] + +data FWit (f :: * -> *) = FWit + +class RowMap (f :: * -> *) (r :: Row *) where + type Map f r :: Row * + rmap :: FWit f -> (forall a. a -> f a) -> Rec r -> Rec (Map f r) + +instance RowMapx f r => RowMap f (R r) where + type Map f (R r) = R (RM f r) + rmap = rmap' + +class RowMapx (f :: * -> *) (r :: [LT *]) where + type RM f r :: [LT *] + rmap' :: FWit f -> (forall a. a -> f a) -> Rec (R r) -> Rec (R (RM f r)) + +instance RowMapx f '[] where + type RM f '[] = '[] + rmap' _ _ _ = empty + +instance (KnownSymbol l, RowMapx f t) => RowMapx f (l :-> v ': t) where + type RM f (l :-> v ': t) = l :-> f v ': RM f t + rmap' w f r = unsafeInjectFront l (f (r .! l)) (rmap' w f (r .- l)) + where l = Label :: Label l + +class RowMapC (c :: * -> Constraint) (f :: * -> *) (r :: Row *) where + type MapC c f r :: Row * + rmapc :: CWit c -> FWit f -> (forall a. c a => a -> f a) -> Rec r -> Rec (MapC c f r) + +instance RMapc c f r => RowMapC c f (R r) where + type MapC c f (R r) = R (RMapp c f r) + rmapc = rmapc' + +class RMapc (c :: * -> Constraint) (f :: * -> *) (r :: [LT *]) where + type RMapp c f r :: [LT *] + rmapc' :: CWit c -> FWit f -> (forall a. c a => a -> f a) -> Rec (R r) -> Rec (R (RMapp c f r)) + +instance RMapc c f '[] where + type RMapp c f '[] = '[] + rmapc' _ _ _ _ = empty + +instance (KnownSymbol l, c v, RMapc c f t) => RMapc c f (l :-> v ': t) where + type RMapp c f (l :-> v ': t) = l :-> f v ': RMapp c f t + rmapc' c w f r = unsafeInjectFront l (f (r .! l)) (rmapc' c w f (r .- l)) + where l = Label :: Label l + +instance Forall (R '[]) c where + rinit _ _ = empty + erase _ _ _ = [] + eraseZip _ _ _ _ = [] + +instance (KnownSymbol l, Forall (R t) c, c a) => Forall (R (l :-> a ': t)) c where + rinit c f = unsafeInjectFront l f (rinit c f) where l = Label :: Label l + + erase c f r = f (r .! l) : erase c f (r .- l) where l = Label :: Label l + + eraseZip c f x y = (f (x .! l) (y .! l)) : eraseZip c f (x .- l) (y .- l) where + l = Label :: Label l + +class RowZip (r1 :: Row *) (r2 :: Row *) where + type RZip r1 r2 :: Row * + rzip :: Rec r1 -> Rec r2 -> Rec (RZip r1 r2) + +instance RZipt r1 r2 => RowZip (R r1) (R r2) where + type RZip (R r1) (R r2) = R (RZipp r1 r2) + rzip = rzip' + +class RZipt (r1 :: [LT *]) (r2 :: [LT *]) where + type RZipp r1 r2 :: [LT *] + rzip' :: Rec (R r1) -> Rec (R r2) -> Rec (R (RZipp r1 r2)) + +instance RZipt '[] '[] where + type RZipp '[] '[] = '[] + rzip' _ _ = empty + +instance (KnownSymbol l, RZipt t1 t2) => + RZipt (l :-> v1 ': t1) (l :-> v2 ': t2) where + + type RZipp (l :-> v1 ': t1) (l :-> v2 ': t2) = l :-> (v1,v2) ': RZipp t1 t2 + rzip' r1 r2 = unsafeInjectFront l (r1 .! l, r2 .! l) (rzip' (r1 .- l) (r2 .- l)) + where l = Label :: Label l + +-- some standard type classes + +instance (Labels r, Forall r Show) => Show (Rec r) where + show r = "{ " ++ meat ++ " }" + where meat = intercalate ", " binds + binds = zipWith (\x y -> x ++ "=" ++ y) ls vs + ls = labels r + vs = erase (CWit :: CWit Show) show r + +instance (Forall r Eq) => Eq (Rec r) where + r == r' = and $ eraseZip (CWit :: CWit Eq) (==) r r' + +instance (Eq (Rec r), Forall r Ord) => Ord (Rec r) where + compare m m' = cmp $ eraseZip (CWit :: CWit Ord) compare m m' + where cmp l | [] <- l' = EQ + | a : _ <- l' = a + where l' = dropWhile (== EQ) l + + +instance (Forall r Bounded) => Bounded (Rec r) where + minBound = rinit (CWit :: CWit Bounded) minBound + maxBound = rinit (CWit :: CWit Bounded) maxBound + +unsafeInjectFront :: KnownSymbol l => Label l -> a -> Rec (R r) -> Rec (R (l :-> a ': r)) +unsafeInjectFront (show -> a) b (OR m) = OR $ M.insert a v m + where v = HideType b <| M.lookupDefault S.empty a m + + +data LT a = Symbol :-> a + +-- gives nicer error message than Bool +data Unique = LabelUnique Symbol | LabelNotUnique Symbol + + + +type family Inject (l :: LT *) (r :: [LT *]) where + Inject (l :-> t) '[] = (l :-> t ': '[]) + Inject (l :-> t) (l' :-> t' ': x) = + Ifte (l <=.? l') + (l :-> t ': l' :-> t' ': x) + (l' :-> t' ': Inject (l :-> t) x) + +type family Ifte (c :: Bool) (t :: [LT *]) (f :: [LT *]) where + Ifte True t f = t + Ifte False t f = f + +data NoSuchField (s :: Symbol) + +type family Get (l :: Symbol) (r :: [LT *]) where + Get l '[] = NoSuchField l + Get l (l :-> t ': x) = t + Get l (l' :-> t ': x) = Get l x + +type family Remove (l :: Symbol) (r :: [LT *]) where + Remove l (l :-> t ': x) = x + Remove l (l' :-> t ': x) = l' :-> t ': Remove l x + +type family LacksP (l :: Symbol) (r :: Row *) where + LacksP l (R r) = LacksR l r + +type family LacksR (l :: Symbol) (r :: [LT *]) where + LacksR l '[] = LabelUnique l + LacksR l (l :-> t ': x) = LabelNotUnique l + LacksR l (p ': x) = LacksR l x + +type family Merge (l :: [LT *]) (r :: [LT *]) where + Merge '[] r = r + Merge l '[] = l + Merge (hl :-> al ': tl) (hr :-> ar ': tr) = + Ifte (hl <=.? hr) + (hl :-> al ': Merge tl (hr :-> ar ': tr)) + (hr :-> ar ': Merge (hl :-> al ': tl) tr) + +-- gives nicer error message than Bool +data DisjointErr = IsDisjoint | Duplicate Symbol + +type family IfteD (c :: Bool) (t :: DisjointErr) (f :: DisjointErr) where + IfteD True t f = t + IfteD False t f = f + +type family DisjointR (l :: Row *) (r :: Row *) where + DisjointR (R l) (R r) = DisjointZ l r + +type family DisjointZ (l :: [LT *]) (r :: [LT *]) where + DisjointZ '[] r = IsDisjoint + DisjointZ l '[] = IsDisjoint + DisjointZ (l :-> al ': tl) (l :-> ar ': tr) = Duplicate l + DisjointZ (hl :-> al ': tl) (hr :-> ar ': tr) = + IfteD (hl <=.? hr) + (DisjointZ tl (hr :-> ar ': tr)) + (DisjointZ (hl :-> al ': tl) tr) + + +-- | there doesn't seem to be a (<=.?) :: Symbol -> Symbol -> Bool, +-- so here it is in terms of other ghc-7.8 type functions +type a <=.? b = (CmpSymbol a b == 'LT) diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,10 @@ +Copyright (c) 2013, Atze van der Ploeg +All rights reserved. + +Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: + +1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. + +2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. + +3. Neither the name of the Atze van der Ploeg nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain