first-class-families (empty) → 0.1.0.0

raw patch · 5 files changed

+219/−0 lines, 5 filesdep +basesetup-changed

Dependencies added: base

Files

LICENSE +19/−0
README.md +8/−0
Setup.hs +2/−0
first-class-families.cabal +34/−0
src/Fcf.hs +156/−0

+ LICENSE view

@@ -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.

+ README.md view

@@ -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)!

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ first-class-families.cabal view

@@ -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

+ src/Fcf.hs view

@@ -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