summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorlyxia <>2018-09-28 02:37:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2018-09-28 02:37:00 (GMT)
commit4c8b8ff38ca4ab576f9d620171e2638eab26ca46 (patch)
treebefa507050298910e9bf481b7379f22582fbfa30
parentaf914249ddd43cc92b70dad7ab5986710898682b (diff)
version 0.3.0.00.3.0.0
-rw-r--r--CHANGELOG.md6
-rw-r--r--first-class-families.cabal2
-rw-r--r--src/Fcf.hs96
3 files changed, 93 insertions, 11 deletions
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 94a49da..d33ccf2 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,10 @@
+# 0.3.0.0
+
+- More new functions, thanks to isovector
+
# 0.2.0.0
-- A whole bunch of basic functions, thanks to @isovector
+- A whole bunch of basic functions, thanks to isovector
- Remove `Traverse` (now `Map`), `BimapPair`, `BimapEither` (now `Bimap`)
# 0.1.0.0
diff --git a/first-class-families.cabal b/first-class-families.cabal
index ecac51a..d44ad79 100644
--- a/first-class-families.cabal
+++ b/first-class-families.cabal
@@ -1,5 +1,5 @@
name: first-class-families
-version: 0.2.0.0
+version: 0.3.0.0
synopsis:
First class type families
description:
diff --git a/src/Fcf.hs b/src/Fcf.hs
index 67e8dc5..c0228f5 100644
--- a/src/Fcf.hs
+++ b/src/Fcf.hs
@@ -28,11 +28,22 @@
--
-- - Fcfs can be higher-order.
-- - The kind constructor 'Exp' is a monad: there's @('=<<')@ and 'Pure'.
+--
+-- Essential language extensions for "Fcf":
+--
+-- > {-# LANGUAGE
+-- > DataKinds,
+-- > PolyKinds,
+-- > TypeFamilies,
+-- > TypeInType,
+-- > TypeOperators,
+-- > UndecidableInstances #-}
module Fcf where
import Data.Kind (Type, Constraint)
-import GHC.TypeLits (Symbol, Nat, type (+), TypeError, ErrorMessage(..))
+import GHC.TypeLits (Symbol, Nat, TypeError, ErrorMessage(..))
+import qualified GHC.TypeLits as TL
-- * First-class type families
@@ -86,10 +97,6 @@ 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 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 ConstFn :: a -> b -> Exp a
type instance Eval (ConstFn a _b) = a
@@ -142,7 +149,7 @@ type instance Eval (Null (a ': as)) = 'False
data Length :: [a] -> Exp Nat
type instance Eval (Length '[]) = 0
-type instance Eval (Length (a ': as)) = 1 + Eval (Length as)
+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
@@ -151,13 +158,32 @@ type instance Eval (Find p (a ': as)) =
('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 '[]) = '[]
@@ -176,6 +202,34 @@ 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.
@@ -206,6 +260,8 @@ 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@.
--
@@ -219,8 +275,6 @@ 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
--- ** Primitives
-
infixr 2 ||
infixr 3 &&
@@ -236,6 +290,24 @@ 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
+
+-- ** Nat
+
+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 ((*) a b) = a TL.* b
+
+data (^) :: Nat -> Nat -> Exp Nat
+type instance Eval ((^) a b) = a TL.^ b
+
-- ** Other
data Error :: Symbol -> Exp a
@@ -253,9 +325,15 @@ type family TyEqImpl (a :: k) (b :: k) :: Bool where
TyEqImpl a b = 'False
infixr 0 $
+
+-- | 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)
+-- | A stuck type that can be used like a type-level 'undefined'.
+type family Stuck :: a
+
-- * Helpful shorthands
-- | Apply and evaluate a unary type function.