first-class-families 0.4.0.0 → 0.5.0.0

raw patch · 11 files changed

+705/−344 lines, 11 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +11/−0
• first-class-families.cabal +11/−2
• src/Fcf.hs +90/−342
• src/Fcf/Classes.hs +49/−0
• src/Fcf/Combinators.hs +81/−0
• src/Fcf/Core.hs +30/−0
• src/Fcf/Data/Bool.hs +88/−0
• src/Fcf/Data/Common.hs +80/−0
• src/Fcf/Data/List.hs +144/−0
• src/Fcf/Data/Nat.hs +61/−0
• src/Fcf/Utils.hs +60/−0

@@ -1,3 +1,14 @@+# 0.5.0.0++- Modularized library++- `Fcf.Utils`:++    + Added `TError`+    + Renamed `Collapse` to `Constraints`++- `Fcf.Data.List`: Added `Cons`, `Last`, `Init`, `Elem`+ # 0.4.0.0  - New functions (blmage)

@@ -1,5 +1,5 @@ name:                first-class-families-version:             0.4.0.0+version:             0.5.0.0 synopsis:   First class type families description:@@ -24,8 +24,17 @@   hs-source-dirs:      src   exposed-modules:     Fcf+    Fcf.Core+    Fcf.Combinators+    Fcf.Data.Bool+    Fcf.Data.Common+    Fcf.Data.List+    Fcf.Data.Nat+    Fcf.Classes+    Fcf.Utils   build-depends:-    base >= 4.9 && < 5+    -- This upper bound is conservative.+    base >= 4.9 && < 4.13   ghc-options:         -Wall   default-language:    Haskell2010 

@@ -1,12 +1,4 @@-{-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-}-{-# LANGUAGE UndecidableInstances #-}  -- | First-class type families --@@ -39,361 +31,117 @@ -- >     TypeOperators, -- >     UndecidableInstances #-} -module Fcf where--import Data.Kind (Type, Constraint)-import GHC.TypeLits (Symbol, Nat, TypeError, ErrorMessage(..))-import qualified GHC.TypeLits as TL---- * First-class type families---- | Kind of type-level expressions indexed by their result type.-type Exp a = a -> Type---- | Expression evaluator.-type family Eval (e :: Exp a) :: a---- ** Monadic operations--infixr 1 =<<, <=<-infixl 4 <$>, <*>--data Pure :: a -> Exp a-type instance Eval (Pure x) = x--data Pure1 :: (a -> b) -> a -> Exp b-type instance Eval (Pure1 f x) = f x--data Pure2 :: (a -> b -> c) -> a -> b -> Exp c-type instance Eval (Pure2 f x y) = f x y--data Pure3 :: (a -> b -> c -> d) -> a -> b -> c -> Exp d-type instance Eval (Pure3 f x y z) = f x y z--data (=<<) :: (a -> Exp b) -> Exp a -> Exp b-type instance Eval (k =<< e) = Eval (k (Eval e))--data (<=<) :: (b -> Exp c) -> (a -> Exp b) -> a -> Exp c-type instance Eval ((f <=< g) x) = Eval (f (Eval (g x)))--type LiftM = (=<<)--data LiftM2 :: (a -> b -> Exp c) -> Exp a -> Exp b -> Exp c-type instance Eval (LiftM2 f x y) = Eval (f (Eval x) (Eval y))--data LiftM3 :: (a -> b -> c -> Exp d) -> Exp a -> Exp b -> Exp c -> Exp d-type instance Eval (LiftM3 f x y z) = Eval (f (Eval x) (Eval y) (Eval z))--data Join :: Exp (Exp a) -> Exp a-type instance Eval (Join e) = Eval (Eval e)--data (<$>) :: (a -> b) -> Exp a -> Exp b-type instance Eval (f <$> e) = f (Eval e)--data (<*>) :: Exp (a -> b) -> Exp a -> Exp b-type instance Eval (f <*> e) = Eval f (Eval e)---- ** More combinators--data Flip :: (a -> b -> Exp c) -> b -> a -> Exp c-type instance Eval (Flip f y x) = Eval (f x y)--data Uncurry :: (a -> b -> Exp c) -> (a, b) -> Exp c-type instance Eval (Uncurry f '(x, y)) = Eval (f x y)--data UnEither :: (a -> Exp c) -> (b -> Exp c) -> Either a b -> Exp c-type instance Eval (UnEither f g ('Left  x)) = Eval (f x)-type instance Eval (UnEither f g ('Right y)) = Eval (g y)--data ConstFn :: a -> b -> Exp a-type instance Eval (ConstFn a _b) = a---- ** Tuples--data Fst :: (a, b) -> Exp a-type instance Eval (Fst '(a, _b)) = a--data Snd :: (a, b) -> Exp b-type instance Eval (Snd '(_a, b)) = b--infixr 3 ***---- | Equivalent to 'Bimap'.-data (***) :: (b -> Exp c) -> (b' -> Exp c') -> (b, b') -> Exp (c, c')-type instance Eval ((***) f f' '(b, b')) = '(Eval (f b), Eval (f' b'))---- ** Lists--data Foldr :: (a -> b -> Exp b) -> b -> [a] -> Exp b-type instance Eval (Foldr f y '[]) = y-type instance Eval (Foldr f y (x ': xs)) = Eval (f x (Eval (Foldr f y xs)))---- | N.B.: This is equivalent to a 'Foldr' flipped.-data UnList :: b -> (a -> b -> Exp b) -> [a] -> Exp b-type instance Eval (UnList y f xs) = Eval (Foldr f y xs)--data (++) :: [a] -> [a] -> Exp [a]-type instance Eval ((++) '[] ys) = ys-type instance Eval ((++) (x ': xs) ys) = x ': Eval ((++) xs ys)--data Filter :: (a -> Exp Bool) -> [a] -> Exp [a]-type instance Eval (Filter _p '[]) = '[]-type instance Eval (Filter p (a ': as)) =-  If (Eval (p a))-    (a ': Eval (Filter p as))-    (Eval (Filter p as))--data Head :: [a] -> Exp (Maybe a)-type instance Eval (Head '[]) = 'Nothing-type instance Eval (Head (a ': _as)) = 'Just a--data Tail :: [a] -> Exp (Maybe [a])-type instance Eval (Tail '[]) = 'Nothing-type instance Eval (Tail (_a ': as)) = 'Just as--data Null :: [a] -> Exp Bool-type instance Eval (Null '[]) = 'True-type instance Eval (Null (a ': as)) = 'False--data Length :: [a] -> Exp Nat-type instance Eval (Length '[]) = 0-type instance Eval (Length (a ': as)) = 1 TL.+ Eval (Length as)--data Find :: (a -> Exp Bool) -> [a] -> Exp (Maybe a)-type instance Eval (Find _p '[]) = 'Nothing-type instance Eval (Find p (a ': as)) =-  If (Eval (p a))-    ('Just a)-    (Eval (Find p as))---- | Find the index of an element satisfying the predicate.-data FindIndex :: (a -> Exp Bool) -> [a] -> Exp (Maybe Nat)-type instance Eval (FindIndex _p '[]) = 'Nothing-type instance Eval (FindIndex p (a ': as)) =-  Eval (If (Eval (p a))-    (Pure ('Just 0))-    (Map ((+) 1) =<< FindIndex p as))---- | Find an element associated with a key.--- @--- 'Lookup' :: k -> [(k, b)] -> 'Exp' ('Maybe' b)--- @-type Lookup (a :: k) (as :: [(k, b)]) =-  (Map Snd (Eval (Find (TyEq a <=< Fst) as)) :: Exp (Maybe b))---- | Modify an element at a given index.------ The list is unchanged if the index is out of bounds.-data SetIndex :: Nat -> a -> [a] -> Exp [a]-type instance Eval (SetIndex n a' as) = SetIndexImpl n a' as--type family SetIndexImpl (n :: Nat) (a' :: k) (as :: [k]) where-  SetIndexImpl _n _a' '[] = '[]-  SetIndexImpl 0 a' (_a ': as) = a' ': as-  SetIndexImpl n a' (a ': as) = a ': SetIndexImpl (n TL.- 1) a' as--data ZipWith :: (a -> b -> Exp c) -> [a] -> [b] -> Exp [c]-type instance Eval (ZipWith _f '[] _bs) = '[]-type instance Eval (ZipWith _f _as '[]) = '[]-type instance Eval (ZipWith f (a ': as) (b ': bs)) =-  Eval (f a b) ': Eval (ZipWith f as bs)---- |--- @--- 'Zip' :: [a] -> [b] -> 'Exp' [(a, b)]--- @-type Zip = ZipWith (Pure2 '(,))--data Unzip :: Exp [(a, b)] -> Exp ([a], [b])-type instance Eval (Unzip as) = Eval (Foldr Cons2 '( '[], '[]) (Eval as))--data Cons2 :: (a, b) -> ([a], [b]) -> Exp ([a], [b])-type instance Eval (Cons2 '(a, b) '(as, bs)) = '(a ': as, b ': bs)---- ** Maybe--data UnMaybe :: Exp b -> (a -> Exp b) -> Maybe a -> Exp b-type instance Eval (UnMaybe y f 'Nothing) = Eval y-type instance Eval (UnMaybe y f ('Just x)) = Eval (f x)--data FromMaybe :: k -> Maybe k -> Exp k-type instance Eval (FromMaybe a 'Nothing)   = a-type instance Eval (FromMaybe _a ('Just b)) = b--data IsJust :: Maybe a -> Exp Bool-type instance Eval (IsJust ('Just _a)) = 'True-type instance Eval (IsJust 'Nothing) = 'False--data IsNothing :: Maybe a -> Exp Bool-type instance Eval (IsNothing ('Just _a)) = 'False-type instance Eval (IsNothing 'Nothing) = 'True---- ** Either--data IsLeft :: Either a b -> Exp Bool-type instance Eval (IsLeft ('Left _a)) = 'True-type instance Eval (IsLeft ('Right _a)) = 'False--data IsRight :: Either a b -> Exp Bool-type instance Eval (IsRight ('Left _a)) = 'False-type instance Eval (IsRight ('Right _a)) = 'True---- ** Overloaded functions---- | Type-level 'fmap' for type-level functors.-data Map :: (a -> Exp b) -> f a -> Exp (f b)--type instance Eval (Map f '[]) = '[]-type instance Eval (Map f (a ': as)) = Eval (f a) ': Eval (Map f as)--type instance Eval (Map f 'Nothing) = 'Nothing-type instance Eval (Map f ('Just a)) = 'Just (Eval (f a))--type instance Eval (Map f ('Left x)) = 'Left x-type instance Eval (Map f ('Right a)) = 'Right (Eval (f a))--type instance Eval (Map f '(x, a)) =-  '(x, Eval (f a))-type instance Eval (Map f '(x, y, a)) =-  '(x, y, Eval (f a))-type instance Eval (Map f '(x, y, z, a)) =-  '(x, y, z, Eval (f a))-type instance Eval (Map f '(x, y, z, w, a)) =-  '(x, y, z, w, Eval (f a))--data Bimap :: (a -> Exp a') -> (b -> Exp b') -> f a b -> Exp (f a' b')--type instance Eval (Bimap f g '(x, y)) = '(Eval (f x), Eval (g y))--type instance Eval (Bimap f g ('Left  x)) = 'Left  (Eval (f x))-type instance Eval (Bimap f g ('Right y)) = 'Right (Eval (g y))---- ** Bool---- | N.B.: The order of the two branches is the opposite of "if":--- @UnBool ifFalse ifTrue bool@.------ This mirrors the default order of constructors:------ @--- data Bool = False | True--- ----------- False < True--- @-data UnBool :: Exp a -> Exp a -> Bool -> Exp a-type instance Eval (UnBool fal tru 'False) = Eval fal-type instance Eval (UnBool fal tru 'True ) = Eval tru--infixr 2 ||-infixr 3 &&--data (||) :: Bool -> Bool -> Exp Bool-type instance Eval ('True || b) = 'True-type instance Eval (a || 'True) = 'True-type instance Eval ('False || b) = b-type instance Eval (a || 'False) = a--data (&&) :: Bool -> Bool -> Exp Bool-type instance Eval ('False && b) = 'False-type instance Eval (a && 'False) = 'False-type instance Eval ('True && b) = b-type instance Eval (a && 'True) = a--data Not :: Bool -> Exp Bool-type instance Eval (Not 'True)  = 'False-type instance Eval (Not 'False) = 'True---- | A conditional choosing the first branch whose guard @a -> 'Exp' 'Bool'@--- accepts a given value @a@.------ === Example------ @--- type UnitPrefix n = 'Eval' ('Guarded' n---   '[ 'TyEq' 0 \'':=' 'Pure' \"\"---    , 'TyEq' 1 \'':=' 'Pure' \"deci\"---    , 'TyEq' 2 \'':=' 'Pure' \"hecto\"---    , 'TyEq' 3 \'':=' 'Pure' \"kilo\"---    , 'TyEq' 6 \'':=' 'Pure' \"mega\"---    , 'TyEq' 9 \'':=' 'Pure' \"giga\"---    , 'Otherwise' \'':=' 'Error' "Something else"---    ])--- @-data Guarded :: a -> [Guard (a -> Exp Bool) (Exp b)] -> Exp b-type instance Eval (Guarded x ((p ':= y) ': ys)) =-    Eval (If (Eval (p x)) y (Guarded x ys))---- | A fancy-looking pair type to use with 'Guarded'.-data Guard a b = a := b-infixr 0 :=+module Fcf+  ( -- * First-class type families --- | A catch-all guard for 'Guarded'.-type Otherwise = ConstFn 'True+    Exp+  , Eval+  , type (@@) --- ** Nat+    -- ** Functional combinators -data (+) :: Nat -> Nat -> Exp Nat-type instance Eval ((+) a b) = a TL.+ b+  , Pure+  , Pure1+  , Pure2+  , Pure3+  , type (=<<)+  , type (<=<)+  , LiftM+  , LiftM2+  , LiftM3+  , Join+  , type (<$>)+  , type (<*>)+  , Flip+  , ConstFn+  , type ($) -data (-) :: Nat -> Nat -> Exp Nat-type instance Eval ((-) a b) = a TL.- b+    -- * Operations on common types -data (*) :: Nat -> Nat -> Exp Nat-type instance Eval ((Fcf.*) a b) = a TL.* b+    -- ** Pairs -data (^) :: Nat -> Nat -> Exp Nat-type instance Eval ((^) a b) = a TL.^ b+  , Uncurry+  , Fst+  , Snd+  , type (***) -data (<=) :: Nat -> Nat -> Exp Bool-type instance Eval ((<=) a b) = a TL.<=? b+    -- ** Either -data (>=) :: Nat -> Nat -> Exp Bool-type instance Eval ((>=) a b) = b TL.<=? a+  , UnEither+  , IsLeft+  , IsRight -data (<) :: Nat -> Nat -> Exp Bool-type instance Eval ((<) a b) = Eval (Not =<< (a >= b))+    -- ** Maybe -data (>) :: Nat -> Nat -> Exp Bool-type instance Eval ((>) a b) = Eval (Not =<< (a <= b))+  , UnMaybe+  , FromMaybe+  , IsNothing+  , IsJust --- ** Other+    -- ** Lists -data Error :: Symbol -> Exp a-type instance Eval (Error msg) = TypeError ('Text msg)+  , Foldr+  , UnList+  , type (++)+  , Filter+  , Head+  , Tail+  , Null+  , Length+  , Find+  , FindIndex+  , Lookup+  , SetIndex+  , ZipWith+  , Zip+  , Unzip+  , Cons2 -data Collapse :: [Constraint] -> Exp Constraint-type instance Eval (Collapse '[]) = () ~ ()-type instance Eval (Collapse (a ': as)) = (a, Eval (Collapse as))+    -- ** Bool -data TyEq :: a -> b -> Exp Bool-type instance Eval (TyEq a b) = TyEqImpl a b+  , UnBool+  , type (||)+  , type (&&)+  , Not -type family TyEqImpl (a :: k) (b :: k) :: Bool where-  TyEqImpl a a = 'True-  TyEqImpl a b = 'False+    -- *** Multi-way if -infixr 0 $+  , Guarded+  , Guard((:=))+  , Otherwise --- | Note that this denotes the identity function, so @($) f@ can usually be--- replaced with @f@.-data ($) :: (a -> Exp b) -> a -> Exp b-type instance Eval (($) f a) = Eval (f a)+    -- ** Nat --- | A stuck type that can be used like a type-level 'undefined'.-type family Stuck :: a+  , type (+)+  , type (-)+  , type (Fcf.Data.Nat.*)+  , type (^)+  , type (<=)+  , type (>=)+  , type (<)+  , type (>) --- * Helpful shorthands+    -- * Overloaded operations --- | Apply and evaluate a unary type function.-type f @@ x = Eval (f x)+  , Map+  , Bimap --- * Reification+    -- * Miscellaneous -class IsBool (b :: Bool) where-  _If :: ((b ~ 'True) => r) -> ((b ~ 'False) => r) -> r+  , Error+  , Constraints+  , TyEq+  , Stuck+  , IsBool(_If)+  , If -instance IsBool 'True  where _If a _ = a-instance IsBool 'False where _If _ b = b+  ) where -type family   If (b :: Bool) (x :: k) (y :: k) :: k-type instance If 'True   x _y = x-type instance If 'False _x  y = y+import Fcf.Core+import Fcf.Combinators+import Fcf.Data.Bool+import Fcf.Data.Common+import Fcf.Data.List+import Fcf.Data.Nat+import Fcf.Classes+import Fcf.Utils

@@ -0,0 +1,49 @@+{-# LANGUAGE+    DataKinds,+    PolyKinds,+    TypeFamilies,+    TypeInType,+    TypeOperators #-}++-- | Overloaded functions.+module Fcf.Classes+  ( Map+  , Bimap+  ) where++import Fcf.Core++-- | Type-level 'fmap' for type-level functors.+data Map :: (a -> Exp b) -> f a -> Exp (f b)++-- []+type instance Eval (Map f '[]) = '[]+type instance Eval (Map f (a ': as)) = Eval (f a) ': Eval (Map f as)++-- Maybe+type instance Eval (Map f 'Nothing) = 'Nothing+type instance Eval (Map f ('Just a)) = 'Just (Eval (f a))++-- Either+type instance Eval (Map f ('Left x)) = 'Left x+type instance Eval (Map f ('Right a)) = 'Right (Eval (f a))++-- Tuples+type instance Eval (Map f '(x, a)) =+  '(x, Eval (f a))+type instance Eval (Map f '(x, y, a)) =+  '(x, y, Eval (f a))+type instance Eval (Map f '(x, y, z, a)) =+  '(x, y, z, Eval (f a))+type instance Eval (Map f '(x, y, z, w, a)) =+  '(x, y, z, w, Eval (f a))++-- | Type-level 'Data.Bifunctor.bimap'.+data Bimap :: (a -> Exp a') -> (b -> Exp b') -> f a b -> Exp (f a' b')++-- (,)+type instance Eval (Bimap f g '(x, y)) = '(Eval (f x), Eval (g y))++-- Either+type instance Eval (Bimap f g ('Left  x)) = 'Left  (Eval (f x))+type instance Eval (Bimap f g ('Right y)) = 'Right (Eval (g y))

@@ -0,0 +1,81 @@+{-# LANGUAGE+    DataKinds,+    PolyKinds,+    TypeFamilies,+    TypeInType,+    TypeOperators,+    UndecidableInstances #-}++-- | General fcf combinators.+module Fcf.Combinators+  ( Pure+  , Pure1+  , Pure2+  , Pure3+  , type (=<<)+  , type (<=<)+  , LiftM+  , LiftM2+  , LiftM3+  , Join+  , type (<$>)+  , type (<*>)+  , Flip+  , ConstFn+  , type ($)+  ) where++import Fcf.Core++-- ** Monadic operations++infixr 1 =<<, <=<+infixl 4 <$>, <*>++data Pure :: a -> Exp a+type instance Eval (Pure x) = x++data Pure1 :: (a -> b) -> a -> Exp b+type instance Eval (Pure1 f x) = f x++data Pure2 :: (a -> b -> c) -> a -> b -> Exp c+type instance Eval (Pure2 f x y) = f x y++data Pure3 :: (a -> b -> c -> d) -> a -> b -> c -> Exp d+type instance Eval (Pure3 f x y z) = f x y z++data (=<<) :: (a -> Exp b) -> Exp a -> Exp b+type instance Eval (k =<< e) = Eval (k (Eval e))++data (<=<) :: (b -> Exp c) -> (a -> Exp b) -> a -> Exp c+type instance Eval ((f <=< g) x) = Eval (f (Eval (g x)))++type LiftM = (=<<)++data LiftM2 :: (a -> b -> Exp c) -> Exp a -> Exp b -> Exp c+type instance Eval (LiftM2 f x y) = Eval (f (Eval x) (Eval y))++data LiftM3 :: (a -> b -> c -> Exp d) -> Exp a -> Exp b -> Exp c -> Exp d+type instance Eval (LiftM3 f x y z) = Eval (f (Eval x) (Eval y) (Eval z))++data Join :: Exp (Exp a) -> Exp a+type instance Eval (Join e) = Eval (Eval e)++data (<$>) :: (a -> b) -> Exp a -> Exp b+type instance Eval (f <$> e) = f (Eval e)++data (<*>) :: Exp (a -> b) -> Exp a -> Exp b+type instance Eval (f <*> e) = Eval f (Eval e)++data Flip :: (a -> b -> Exp c) -> b -> a -> Exp c+type instance Eval (Flip f y x) = Eval (f x y)++data ConstFn :: a -> b -> Exp a+type instance Eval (ConstFn a _b) = a++-- | Note that this denotes the identity function, so @($) f@ can usually be+-- replaced with @f@.+data ($) :: (a -> Exp b) -> a -> Exp b+type instance Eval (($) f a) = Eval (f a)++infixr 0 $

@@ -0,0 +1,30 @@+{-# LANGUAGE+    DataKinds,+    PolyKinds,+    TypeFamilies,+    TypeInType,+    TypeOperators #-}++-- | The 'Eval' family.++module Fcf.Core+  ( Exp+  , Eval+  , type (@@)+  ) where++import Data.Kind (Type)++-- * First-class type families++-- | Kind of type-level expressions indexed by their result type.+type Exp a = a -> Type++-- | Expression evaluator.+type family Eval (e :: Exp a) :: a++-- ** Miscellaneous++-- | Apply and evaluate a unary type function.+type f @@ x = Eval (f x)+

@@ -0,0 +1,88 @@+{-# LANGUAGE+    DataKinds,+    PolyKinds,+    TypeFamilies,+    TypeInType,+    TypeOperators,+    UndecidableInstances #-}++-- | Booleans.+--+-- Note that the operations from this module conflict with+-- "Data.Type.Bool".+module Fcf.Data.Bool+  ( UnBool+  , type (||)+  , type (&&)+  , Not++    -- *** Multi-way if++  , Guarded+  , Guard((:=))+  , Otherwise+  ) where++import Fcf.Core+import Fcf.Combinators (ConstFn)+import Fcf.Utils++-- | N.B.: The order of the two branches is the opposite of "if":+-- @UnBool ifFalse ifTrue bool@.+--+-- This mirrors the default order of constructors:+--+-- @+-- data Bool = False | True+-- ----------- False < True+-- @+data UnBool :: Exp a -> Exp a -> Bool -> Exp a+type instance Eval (UnBool fal tru 'False) = Eval fal+type instance Eval (UnBool fal tru 'True ) = Eval tru++infixr 2 ||+infixr 3 &&++data (||) :: Bool -> Bool -> Exp Bool+type instance Eval ('True || b) = 'True+type instance Eval (a || 'True) = 'True+type instance Eval ('False || b) = b+type instance Eval (a || 'False) = a++data (&&) :: Bool -> Bool -> Exp Bool+type instance Eval ('False && b) = 'False+type instance Eval (a && 'False) = 'False+type instance Eval ('True && b) = b+type instance Eval (a && 'True) = a++data Not :: Bool -> Exp Bool+type instance Eval (Not 'True)  = 'False+type instance Eval (Not 'False) = 'True++-- | A conditional choosing the first branch whose guard @a -> 'Exp' 'Bool'@+-- accepts a given value @a@.+--+-- === Example+--+-- @+-- type UnitPrefix n = 'Eval' ('Guarded' n+--   '[ 'TyEq' 0 \'':=' 'Pure' \"\"+--    , 'TyEq' 1 \'':=' 'Pure' \"deci\"+--    , 'TyEq' 2 \'':=' 'Pure' \"hecto\"+--    , 'TyEq' 3 \'':=' 'Pure' \"kilo\"+--    , 'TyEq' 6 \'':=' 'Pure' \"mega\"+--    , 'TyEq' 9 \'':=' 'Pure' \"giga\"+--    , 'Otherwise' \'':=' 'Error' "Something else"+--    ])+-- @+data Guarded :: a -> [Guard (a -> Exp Bool) (Exp b)] -> Exp b+type instance Eval (Guarded x ((p ':= y) ': ys)) =+    Eval (If (Eval (p x)) y (Guarded x ys))++-- | A fancy-looking pair type to use with 'Guarded'.+data Guard a b = a := b+infixr 0 :=++-- | A catch-all guard for 'Guarded'.+type Otherwise = ConstFn 'True+

@@ -0,0 +1,80 @@+{-# LANGUAGE+    DataKinds,+    PolyKinds,+    TypeFamilies,+    TypeInType,+    TypeOperators #-}++-- | Common data types: tuples, 'Either', 'Maybe'.+module Fcf.Data.Common+  ( -- ** Pairs++    Uncurry+  , Fst+  , Snd+  , type (***)++    -- ** Either++  , UnEither+  , IsLeft+  , IsRight++    -- ** Maybe++  , UnMaybe+  , FromMaybe+  , IsNothing+  , IsJust+  ) where++import Fcf.Core++-- ** Pairs++data Uncurry :: (a -> b -> Exp c) -> (a, b) -> Exp c+type instance Eval (Uncurry f '(x, y)) = Eval (f x y)++data Fst :: (a, b) -> Exp a+type instance Eval (Fst '(a, _b)) = a++data Snd :: (a, b) -> Exp b+type instance Eval (Snd '(_a, b)) = b++infixr 3 ***++-- | Equivalent to 'Bimap' for pairs.+data (***) :: (b -> Exp c) -> (b' -> Exp c') -> (b, b') -> Exp (c, c')+type instance Eval ((***) f f' '(b, b')) = '(Eval (f b), Eval (f' b'))++-- ** Either++data UnEither :: (a -> Exp c) -> (b -> Exp c) -> Either a b -> Exp c+type instance Eval (UnEither f g ('Left  x)) = Eval (f x)+type instance Eval (UnEither f g ('Right y)) = Eval (g y)++data IsLeft :: Either a b -> Exp Bool+type instance Eval (IsLeft ('Left _a)) = 'True+type instance Eval (IsLeft ('Right _a)) = 'False++data IsRight :: Either a b -> Exp Bool+type instance Eval (IsRight ('Left _a)) = 'False+type instance Eval (IsRight ('Right _a)) = 'True++-- ** Maybe++data UnMaybe :: Exp b -> (a -> Exp b) -> Maybe a -> Exp b+type instance Eval (UnMaybe y f 'Nothing) = Eval y+type instance Eval (UnMaybe y f ('Just x)) = Eval (f x)++data FromMaybe :: k -> Maybe k -> Exp k+type instance Eval (FromMaybe a 'Nothing)   = a+type instance Eval (FromMaybe _a ('Just b)) = b++data IsNothing :: Maybe a -> Exp Bool+type instance Eval (IsNothing ('Just _a)) = 'False+type instance Eval (IsNothing 'Nothing) = 'True++data IsJust :: Maybe a -> Exp Bool+type instance Eval (IsJust ('Just _a)) = 'True+type instance Eval (IsJust 'Nothing) = 'False

@@ -0,0 +1,144 @@+{-# LANGUAGE+    DataKinds,+    PolyKinds,+    TypeFamilies,+    TypeInType,+    TypeOperators,+    UndecidableInstances #-}++-- | Lists.+module Fcf.Data.List+  ( Foldr+  , UnList+  , Cons+  , type (++)+  , Filter+  , Head+  , Last+  , Tail+  , Init+  , Null+  , Length+  , Find+  , FindIndex+  , Elem+  , Lookup+  , SetIndex+  , ZipWith+  , Zip+  , Unzip+  , Cons2+  ) where++import GHC.TypeLits (Nat)+import qualified GHC.TypeLits as TL++import Fcf.Core+import Fcf.Combinators+import Fcf.Classes+import Fcf.Data.Common+import Fcf.Data.Nat+import Fcf.Utils++data Cons :: a -> [a] -> Exp [a]+type instance Eval (Cons a as) = a ': as++data Foldr :: (a -> b -> Exp b) -> b -> [a] -> Exp b+type instance Eval (Foldr f y '[]) = y+type instance Eval (Foldr f y (x ': xs)) = Eval (f x (Eval (Foldr f y xs)))++-- | N.B.: This is equivalent to a 'Foldr' flipped.+data UnList :: b -> (a -> b -> Exp b) -> [a] -> Exp b+type instance Eval (UnList y f xs) = Eval (Foldr f y xs)++data (++) :: [a] -> [a] -> Exp [a]+type instance Eval ((++) '[] ys) = ys+type instance Eval ((++) (x ': xs) ys) = x ': Eval ((++) xs ys)++data Filter :: (a -> Exp Bool) -> [a] -> Exp [a]+type instance Eval (Filter _p '[]) = '[]+type instance Eval (Filter p (a ': as)) =+  If (Eval (p a))+    (a ': Eval (Filter p as))+    (Eval (Filter p as))++data Head :: [a] -> Exp (Maybe a)+type instance Eval (Head '[]) = 'Nothing+type instance Eval (Head (a ': _as)) = 'Just a++data Last :: [a] -> Exp (Maybe a)+type instance Eval (Last '[]) = 'Nothing+type instance Eval (Last (a ': '[])) = 'Just a+type instance Eval (Last (a ': b ': as)) = Eval (Last (b ': as))++data Init :: [a] -> Exp (Maybe [a])+type instance Eval (Init '[]) = 'Nothing+type instance Eval (Init (a ': '[])) = 'Just '[]+type instance Eval (Init (a ': b ': as)) =+  Eval (Map (Cons a) =<< (Init (b ': as)))++data Tail :: [a] -> Exp (Maybe [a])+type instance Eval (Tail '[]) = 'Nothing+type instance Eval (Tail (_a ': as)) = 'Just as++data Null :: [a] -> Exp Bool+type instance Eval (Null '[]) = 'True+type instance Eval (Null (a ': as)) = 'False++data Length :: [a] -> Exp Nat+type instance Eval (Length '[]) = 0+type instance Eval (Length (a ': as)) = 1 TL.+ Eval (Length as)++data Find :: (a -> Exp Bool) -> [a] -> Exp (Maybe a)+type instance Eval (Find _p '[]) = 'Nothing+type instance Eval (Find p (a ': as)) =+  If (Eval (p a))+    ('Just a)+    (Eval (Find p as))++-- | Find the index of an element satisfying the predicate.+data FindIndex :: (a -> Exp Bool) -> [a] -> Exp (Maybe Nat)+type instance Eval (FindIndex _p '[]) = 'Nothing+type instance Eval (FindIndex p (a ': as)) =+  Eval (If (Eval (p a))+    (Pure ('Just 0))+    (Map ((+) 1) =<< FindIndex p as))++type Elem a as = IsJust =<< FindIndex (TyEq a) as++-- | Find an element associated with a key.+-- @+-- 'Lookup' :: k -> [(k, b)] -> 'Exp' ('Maybe' b)+-- @+type Lookup (a :: k) (as :: [(k, b)]) =+  (Map Snd (Eval (Find (TyEq a <=< Fst) as)) :: Exp (Maybe b))++-- | Modify an element at a given index.+--+-- The list is unchanged if the index is out of bounds.+data SetIndex :: Nat -> a -> [a] -> Exp [a]+type instance Eval (SetIndex n a' as) = SetIndexImpl n a' as++type family SetIndexImpl (n :: Nat) (a' :: k) (as :: [k]) where+  SetIndexImpl _n _a' '[] = '[]+  SetIndexImpl 0 a' (_a ': as) = a' ': as+  SetIndexImpl n a' (a ': as) = a ': SetIndexImpl (n TL.- 1) a' as++data ZipWith :: (a -> b -> Exp c) -> [a] -> [b] -> Exp [c]+type instance Eval (ZipWith _f '[] _bs) = '[]+type instance Eval (ZipWith _f _as '[]) = '[]+type instance Eval (ZipWith f (a ': as) (b ': bs)) =+  Eval (f a b) ': Eval (ZipWith f as bs)++-- |+-- @+-- 'Zip' :: [a] -> [b] -> 'Exp' [(a, b)]+-- @+type Zip = ZipWith (Pure2 '(,))++data Unzip :: Exp [(a, b)] -> Exp ([a], [b])+type instance Eval (Unzip as) = Eval (Foldr Cons2 '( '[], '[]) (Eval as))++data Cons2 :: (a, b) -> ([a], [b]) -> Exp ([a], [b])+type instance Eval (Cons2 '(a, b) '(as, bs)) = '(a ': as, b ': bs)+

@@ -0,0 +1,61 @@+{-# LANGUAGE+    DataKinds,+    PolyKinds,+    TypeFamilies,+    TypeInType,+    TypeOperators,+    UndecidableInstances #-}++-- | Natural numbers.+--+-- Note that the operators from this module conflict with "GHC.TypeLits" and+-- "GHC.TypeNats".+module Fcf.Data.Nat+  ( -- * Reexported type+    -- | From "GHC.TypeNats".++    Nat++    -- * Operations++  , type (+)+  , type (-)+  , type (Fcf.Data.Nat.*)+  , type (^)+  , type (<=)+  , type (>=)+  , type (<)+  , type (>)+  ) where++import GHC.TypeLits (Nat)+import qualified GHC.TypeLits as TL++import Fcf.Core+import Fcf.Combinators+import Fcf.Data.Bool (Not)++data (+) :: Nat -> Nat -> Exp Nat+type instance Eval ((+) a b) = a TL.+ b++data (-) :: Nat -> Nat -> Exp Nat+type instance Eval ((-) a b) = a TL.- b++data (*) :: Nat -> Nat -> Exp Nat+type instance Eval ((Fcf.Data.Nat.*) a b) = a TL.* b++data (^) :: Nat -> Nat -> Exp Nat+type instance Eval ((^) a b) = a TL.^ b++data (<=) :: Nat -> Nat -> Exp Bool+type instance Eval ((<=) a b) = a TL.<=? b++data (>=) :: Nat -> Nat -> Exp Bool+type instance Eval ((>=) a b) = b TL.<=? a++data (<) :: Nat -> Nat -> Exp Bool+type instance Eval ((<) a b) = Eval (Not =<< (a >= b))++data (>) :: Nat -> Nat -> Exp Bool+type instance Eval ((>) a b) = Eval (Not =<< (a <= b))+

@@ -0,0 +1,60 @@+{-# LANGUAGE+    AllowAmbiguousTypes,+    ConstraintKinds,+    DataKinds,+    PolyKinds,+    RankNTypes,+    TypeFamilies,+    TypeInType,+    TypeOperators #-}++-- | Miscellaneous families.+module Fcf.Utils+  ( Error+  , TError+  , Constraints+  , TyEq+  , Stuck+  , IsBool(_If)++    -- | From "Data.Type.Bool".+  , If+  ) where++import Data.Kind (Constraint)+import Data.Type.Bool (If)+import GHC.TypeLits (Symbol, TypeError, ErrorMessage(..))++import Fcf.Core++-- | Type-level 'error'.+data Error :: Symbol -> Exp a+type instance Eval (Error msg) = TypeError ('Text msg)++-- | 'TypeError' as a fcf.+data TError :: ErrorMessage -> Exp a+type instance Eval (TError msg) = TypeError msg++-- | Conjunction of a list of constraints.+data Constraints :: [Constraint] -> Exp Constraint+type instance Eval (Constraints '[]) = (() :: Constraint)+type instance Eval (Constraints (a ': as)) = (a, Eval (Constraints as))++-- | Type equality.+data TyEq :: a -> b -> Exp Bool+type instance Eval (TyEq a b) = TyEqImpl a b++type family TyEqImpl (a :: k) (b :: k) :: Bool where+  TyEqImpl a a = 'True+  TyEqImpl a b = 'False++-- | A stuck type that can be used like a type-level 'undefined'.+type family Stuck :: a++-- * Reification++class IsBool (b :: Bool) where+  _If :: ((b ~ 'True) => r) -> ((b ~ 'False) => r) -> r++instance IsBool 'True  where _If a _ = a+instance IsBool 'False where _If _ b = b