summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorlyxia <>2018-07-11 04:38:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2018-07-11 04:38:00 (GMT)
commit2d9b2358238a736737362375977b61294d925e29 (patch)
tree31d97df49ff652047127e5d68d519ae9e5401817
version 0.1.0.00.1.0.0
-rw-r--r--LICENSE19
-rw-r--r--README.md8
-rw-r--r--Setup.hs2
-rw-r--r--first-class-families.cabal34
-rw-r--r--src/Fcf.hs156
5 files changed, 219 insertions, 0 deletions
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..b4a9b96
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,19 @@
+Copyright Li-yao Xia (c) 2018
+
+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. \ No newline at end of file
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..2aa269b
--- /dev/null
+++ b/README.md
@@ -0,0 +1,8 @@
+# First-class type families [![Hackage](https://img.shields.io/hackage/v/first-class-families.svg)](https://hackage.haskell.org/package/first-class-families) [![Build Status](https://travis-ci.org/Lysxia/first-class-families.svg)](https://travis-ci.org/Lysxia/first-class-families)
+
+See `src/Fcf`.
+
+---
+
+Contributions are welcome. Feel free to open an issue or make a PR on
+[Github](https://github.com/Lysxia/first-class-families)!
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
index 0000000..9a994af
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/first-class-families.cabal b/first-class-families.cabal
new file mode 100644
index 0000000..1747666
--- /dev/null
+++ b/first-class-families.cabal
@@ -0,0 +1,34 @@
+name: first-class-families
+version: 0.1.0.0
+synopsis:
+ First class type families
+description:
+ First class type families,
+ eval-style defunctionalization
+ .
+ See "Fcf".
+homepage: https://github.com/Lysxia/first-class-families#readme
+license: MIT
+license-file: LICENSE
+author: Li-yao Xia
+maintainer: lysxia@gmail.com
+copyright: 2018 Li-yao Xia
+category: Other
+build-type: Simple
+extra-source-files: README.md
+cabal-version: >=1.10
+tested-with:
+ GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.3
+
+library
+ hs-source-dirs: src
+ exposed-modules:
+ Fcf
+ build-depends:
+ base >= 4.9 && < 5
+ ghc-options: -Wall
+ default-language: Haskell2010
+
+source-repository head
+ type: git
+ location: https://github.com/Lysxia/first-class-families
diff --git a/src/Fcf.hs b/src/Fcf.hs
new file mode 100644
index 0000000..9b42c2b
--- /dev/null
+++ b/src/Fcf.hs
@@ -0,0 +1,156 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | First-class type families
+--
+-- For example, here is a regular type family:
+--
+-- @
+-- type family FromMaybe (a :: k) (m :: Maybe k) :: k
+-- type instance FromMaybe a 'Nothing = a
+-- type instance FromMaybe a ('Just b) = b
+-- @
+--
+-- With @Fcf@, it translates to a @data@ declaration:
+--
+-- @
+-- data FromMaybe :: k -> Maybe k -> 'Exp' k
+-- type instance 'Eval' (FromMaybe a 'Nothing) = a
+-- type instance 'Eval' (FromMaybe a ('Just b)) = b
+-- @
+--
+-- - Fcfs can be higher-order.
+-- - The kind constructor 'Exp' is a monad: there's @('=<<')@ and 'Pure'.
+
+module Fcf 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
+
+-- ** 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)))
+
+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 higher-order 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 BimapPair :: (a -> Exp a') -> (b -> Exp b') -> (a, b) -> Exp (a', b')
+type instance Eval (BimapPair f g '(x, y)) = '(Eval (f x), Eval (g 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 BimapEither
+ :: (a -> Exp a') -> (b -> Exp b') -> Either a b -> Exp (Either a' b')
+type instance Eval (BimapEither f g ('Left x)) = 'Left (Eval (f x))
+type instance Eval (BimapEither f g ('Right y)) = 'Right (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 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)))
+
+data Traverse :: (a -> Exp b) -> [a] -> Exp [b]
+type instance Eval (Traverse f '[]) = '[]
+type instance Eval (Traverse f (x ': xs)) = Eval (f x) ': Eval (Traverse f 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)
+
+-- | 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
+
+-- ** Primitives
+
+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
+
+-- * Helpful shorthands
+
+-- | Apply and evaluate a unary type function.
+type f @@ x = Eval (f x)
+
+-- * 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
+
+type family If (b :: Bool) (x :: k) (y :: k) :: k
+type instance If 'True x _y = x
+type instance If 'False _x y = y