Safe Haskell	Trustworthy
Language	Haskell2010

DeFun.Core

Contents

FunKind
Fun
App
Lam
Con

Description

Defunctorization core primitives.

Synopsis

data FunKind a b
type Fun a b = FunKind a b -> Type
type (~>) a b = Fun a b
type family App (f :: a ~> b) (x :: a) :: b
type (@@) (a1 :: a ~> k) (b :: a) = App a1 b
newtype Lam (a1 :: a -> Type) (b1 :: b -> Type) (f :: a ~> b) = Lam {
- appLam :: LamRep a1 b1 f
}
type (:~>) (a1 :: a -> Type) (b1 :: b -> Type) = Lam a1 b1
mkLam :: forall {a1} {b1} (a2 :: a1 -> Type) (b2 :: b1 -> Type) (f :: a1 ~> b1). LamRep a2 b2 f -> Lam a2 b2 f
type LamRep (a1 :: a -> Type) (b1 :: b -> Type) (fun :: a ~> b) = forall (x :: a). a1 x -> b1 (fun @@ x)
(@@) :: forall {a1} {k} a2 b (f :: a1 ~> k) (x :: a1). Lam a2 b f -> a2 x -> b (f @@ x)
type Lam2 (a2 :: a -> Type) (b1 :: a1 -> Type) (c :: b -> Type) (fun :: a ~> (a1 ~> b)) = Lam a2 (b1 :~> c) fun
type Lam3 (a3 :: a -> Type) (b1 :: a1 -> Type) (c :: a2 -> Type) (d :: b -> Type) (fun :: a ~> (a1 ~> (a2 ~> b))) = Lam a3 (b1 :~> (c :~> d)) fun
type LamRep2 (a1 :: a -> Type) (b1 :: b -> Type) (c1 :: c -> Type) (fun :: a ~> (b ~> c)) = forall (x :: a) (y :: b). a1 x -> b1 y -> c1 ((fun @@ x) @@ y)
type LamRep3 (a1 :: a -> Type) (b1 :: b -> Type) (c1 :: c -> Type) (d1 :: d -> Type) (fun :: a ~> (b ~> (c ~> d))) = forall (x :: a) (y :: b) (z :: c). a1 x -> b1 y -> c1 z -> d1 (((fun @@ x) @@ y) @@ z)
pattern Lam2 :: LamRep2 a3 b2 c fun -> Lam2 a3 b2 c fun
pattern Lam3 :: LamRep3 a4 b2 c d fun -> Lam3 a4 b2 c d fun
mkLam2 :: forall {a1} {a2} {b1} (a3 :: a1 -> Type) (b2 :: a2 -> Type) (c :: b1 -> Type) (fun :: a1 ~> (a2 ~> b1)). LamRep2 a3 b2 c fun -> Lam2 a3 b2 c fun
appLam2 :: forall {a1} {b1} {c1} (a2 :: a1 -> Type) (b2 :: b1 -> Type) (c2 :: c1 -> Type) (fun :: a1 ~> (b1 ~> c1)). Lam2 a2 b2 c2 fun -> LamRep2 a2 b2 c2 fun
mkLam3 :: forall {a1} {a2} {a3} {b1} (a4 :: a1 -> Type) (b2 :: a2 -> Type) (c :: a3 -> Type) (d :: b1 -> Type) (fun :: a1 ~> (a2 ~> (a3 ~> b1))). LamRep3 a4 b2 c d fun -> Lam3 a4 b2 c d fun
appLam3 :: forall {a1} {b1} {c1} {d1} (a2 :: a1 -> Type) (b2 :: b1 -> Type) (c2 :: c1 -> Type) (d2 :: d1 -> Type) (fun :: a1 ~> (b1 ~> (c1 ~> d1))). Lam3 a2 b2 c2 d2 fun -> LamRep3 a2 b2 c2 d2 fun
data Con1 (con :: a -> b) (arg :: FunKind a b)
data Con2 (con :: a -> b -> c) (arg :: FunKind a (b ~> c))
data Con3 (con :: a -> b -> c -> d) (arg :: FunKind a (b ~> (c ~> d)))
con1 :: forall {a1} {b1} (a2 :: a1 -> Type) (b2 :: b1 -> Type) (con :: a1 -> b1). LamRep a2 b2 (Con1 con) -> Lam a2 b2 (Con1 con)
con2 :: forall {a1} {b1} {c1} (a2 :: a1 -> Type) (b2 :: b1 -> Type) (c2 :: c1 -> Type) (con :: a1 -> b1 -> c1). LamRep2 a2 b2 c2 (Con2 con) -> Lam2 a2 b2 c2 (Con2 con)
con3 :: forall {a1} {b1} {c1} {d1} (a2 :: a1 -> Type) (b2 :: b1 -> Type) (c2 :: c1 -> Type) (d2 :: d1 -> Type) (con :: a1 -> b1 -> c1 -> d1). LamRep3 a2 b2 c2 d2 (Con3 con) -> Lam3 a2 b2 c2 d2 (Con3 con)

Documentation

>>> import Prelude (Show)
>>> import Data.SOP.NP (NP (..))
>>> import DeFun

FunKind

data FunKind a b Source #

A kind for type-level functions.

Instances

Instances details

type App LAndSym (x :: Bool) Source #
Instance details Defined in DeFun.Bool type App LAndSym (x :: Bool) = LAndSym1 x
type App LOrSym (x :: Bool) Source #
Instance details Defined in DeFun.Bool type App LOrSym (x :: Bool) = LOrSym1 x
type App (ConstSym :: FunKind a (b ~> a) -> Type) (x :: a) Source #
Instance details Defined in DeFun.Function type App (ConstSym :: FunKind a (b ~> a) -> Type) (x :: a) = ConstSym1 x :: FunKind b a -> Type
type App (FoldlSym1 f :: FunKind b ([a] ~> b) -> Type) (z :: b) Source #
Instance details Defined in DeFun.List type App (FoldlSym1 f :: FunKind b ([a] ~> b) -> Type) (z :: b) = FoldlSym2 f z
type App (FoldrSym1 f :: FunKind b ([a] ~> b) -> Type) (z :: b) Source #
Instance details Defined in DeFun.List type App (FoldrSym1 f :: FunKind b ([a] ~> b) -> Type) (z :: b) = FoldrSym2 f z
type App (Con2 f :: FunKind a1 (a2 ~> b) -> Type) (arg :: a1) Source #
Instance details Defined in DeFun.Core type App (Con2 f :: FunKind a1 (a2 ~> b) -> Type) (arg :: a1) = Con1 (f arg)
type App (FlipSym1 f :: FunKind b (a ~> c) -> Type) (x :: b) Source #
Instance details Defined in DeFun.Function type App (FlipSym1 f :: FunKind b (a ~> c) -> Type) (x :: b) = FlipSym2 f x
type App (Con3 f :: FunKind a1 (a2 ~> (b ~> c)) -> Type) (arg :: a1) Source #
Instance details Defined in DeFun.Core type App (Con3 f :: FunKind a1 (a2 ~> (b ~> c)) -> Type) (arg :: a1) = Con2 (f arg)
type App (AppendSym :: FunKind [a] ([a] ~> [a]) -> Type) (xs :: [a]) Source #
Instance details Defined in DeFun.List type App (AppendSym :: FunKind [a] ([a] ~> [a]) -> Type) (xs :: [a]) = AppendSym1 xs
type App (Map2Sym1 f :: FunKind [a] ([b] ~> [c]) -> Type) (xs :: [a]) Source #
Instance details Defined in DeFun.List type App (Map2Sym1 f :: FunKind [a] ([b] ~> [c]) -> Type) (xs :: [a]) = Map2Sym2 f xs
type App (ZipWithSym1 f :: FunKind [a] ([b] ~> [c]) -> Type) (xs :: [a]) Source #
Instance details Defined in DeFun.List type App (ZipWithSym1 f :: FunKind [a] ([b] ~> [c]) -> Type) (xs :: [a]) = ZipWithSym2 f xs
type App (FilterSym :: FunKind (a ~> Bool) ([a] ~> [a]) -> Type) (p :: a ~> Bool) Source #
Instance details Defined in DeFun.List type App (FilterSym :: FunKind (a ~> Bool) ([a] ~> [a]) -> Type) (p :: a ~> Bool) = FilterSym1 p
type App (JoinSym :: FunKind (a ~> (a ~> b)) (a ~> b) -> Type) (f :: a ~> (a ~> b)) Source #
Instance details Defined in DeFun.Function type App (JoinSym :: FunKind (a ~> (a ~> b)) (a ~> b) -> Type) (f :: a ~> (a ~> b)) = JoinSym1 f
type App (FoldrSym :: FunKind (a ~> (b ~> b)) (b ~> ([a] ~> b)) -> Type) (f :: a ~> (b ~> b)) Source #
Instance details Defined in DeFun.List type App (FoldrSym :: FunKind (a ~> (b ~> b)) (b ~> ([a] ~> b)) -> Type) (f :: a ~> (b ~> b)) = FoldrSym1 f
type App (ConcatMapSym :: FunKind (a ~> [b]) ([a] ~> [b]) -> Type) (f :: a ~> [b]) Source #
Instance details Defined in DeFun.List type App (ConcatMapSym :: FunKind (a ~> [b]) ([a] ~> [b]) -> Type) (f :: a ~> [b]) = ConcatMapSym1 f
type App (MapSym :: FunKind (a ~> b) ([a] ~> [b]) -> Type) (f :: a ~> b) Source #
Instance details Defined in DeFun.List type App (MapSym :: FunKind (a ~> b) ([a] ~> [b]) -> Type) (f :: a ~> b) = MapSym1 f
type App (FoldlSym :: FunKind (b ~> (a ~> b)) (b ~> ([a] ~> b)) -> Type) (f :: b ~> (a ~> b)) Source #
Instance details Defined in DeFun.List type App (FoldlSym :: FunKind (b ~> (a ~> b)) (b ~> ([a] ~> b)) -> Type) (f :: b ~> (a ~> b)) = FoldlSym1 f
type App (ApSym :: FunKind (a ~> (b ~> c)) ((a ~> b) ~> (a ~> c)) -> Type) (f :: a ~> (b ~> c)) Source #
Instance details Defined in DeFun.Function type App (ApSym :: FunKind (a ~> (b ~> c)) ((a ~> b) ~> (a ~> c)) -> Type) (f :: a ~> (b ~> c)) = ApSym1 f
type App (Map2Sym :: FunKind (a ~> (b ~> c)) ([a] ~> ([b] ~> [c])) -> Type) (f :: a ~> (b ~> c)) Source #
Instance details Defined in DeFun.List type App (Map2Sym :: FunKind (a ~> (b ~> c)) ([a] ~> ([b] ~> [c])) -> Type) (f :: a ~> (b ~> c)) = Map2Sym1 f
type App (ZipWithSym :: FunKind (a ~> (b ~> c)) ([a] ~> ([b] ~> [c])) -> Type) (f :: a ~> (b ~> c)) Source #
Instance details Defined in DeFun.List type App (ZipWithSym :: FunKind (a ~> (b ~> c)) ([a] ~> ([b] ~> [c])) -> Type) (f :: a ~> (b ~> c)) = ZipWithSym1 f
type App (FlipSym :: FunKind (a ~> (b ~> c)) (b ~> (a ~> c)) -> Type) (f :: a ~> (b ~> c)) Source #
Instance details Defined in DeFun.Function type App (FlipSym :: FunKind (a ~> (b ~> c)) (b ~> (a ~> c)) -> Type) (f :: a ~> (b ~> c)) = FlipSym1 f
type App (CompSym :: FunKind (b ~> c) ((a ~> b) ~> (a ~> c)) -> Type) (f :: b ~> c) Source #
Instance details Defined in DeFun.Function type App (CompSym :: FunKind (b ~> c) ((a ~> b) ~> (a ~> c)) -> Type) (f :: b ~> c) = CompSym1 f :: FunKind (a ~> b) (a ~> c) -> Type
type App (ApSym1 f :: FunKind (a ~> b) (a ~> c) -> Type) (g :: a ~> b) Source #
Instance details Defined in DeFun.Function type App (ApSym1 f :: FunKind (a ~> b) (a ~> c) -> Type) (g :: a ~> b) = ApSym2 f g
type App (CompSym1 f :: FunKind (a ~> b) (a ~> c) -> Type) (g :: a ~> b) Source #
Instance details Defined in DeFun.Function type App (CompSym1 f :: FunKind (a ~> b) (a ~> c) -> Type) (g :: a ~> b) = CompSym2 f g

Fun

type Fun a b = FunKind a b -> Type Source #

Something of kind Fun a b (or a ~> b) is a defunctionalized type function.

Normal type arrows (->) can be converted into defunctionalized arrows (~>) by use of Con1, Con2 ... family of types.

type (~>) a b = Fun a b infixr 0 Source #

An infix synonmy for Fun.

App

type family App (f :: a ~> b) (x :: a) :: b Source #

Type level function application.

Instances

Instances details

type App NotSym (x :: Bool) Source #
Instance details Defined in DeFun.Bool type App NotSym (x :: Bool) = Not x
type App (LAndSym1 x :: FunKind Bool Bool -> Type) (y :: Bool) Source #
Instance details Defined in DeFun.Bool type App (LAndSym1 x :: FunKind Bool Bool -> Type) (y :: Bool) = LAnd x y
type App (LOrSym1 x :: FunKind Bool Bool -> Type) (y :: Bool) Source #
Instance details Defined in DeFun.Bool type App (LOrSym1 x :: FunKind Bool Bool -> Type) (y :: Bool) = LOr x y
type App (IdSym :: FunKind a a -> Type) (x :: a) Source #
Instance details Defined in DeFun.Function type App (IdSym :: FunKind a a -> Type) (x :: a) = Id x
type App (Con1 f :: FunKind a b -> Type) (x :: a) Source #
Instance details Defined in DeFun.Core type App (Con1 f :: FunKind a b -> Type) (x :: a) = f x
type App (JoinSym1 f :: FunKind a b -> Type) (x :: a) Source #
Instance details Defined in DeFun.Function type App (JoinSym1 f :: FunKind a b -> Type) (x :: a) = Join f x
type App (ConstSym1 x :: FunKind b a -> Type) (y :: b) Source #
Instance details Defined in DeFun.Function type App (ConstSym1 x :: FunKind b a -> Type) (y :: b) = Const x y
type App (ApSym2 f g :: FunKind a c -> Type) (x :: a) Source #
Instance details Defined in DeFun.Function type App (ApSym2 f g :: FunKind a c -> Type) (x :: a) = Ap f g x
type App (CompSym2 f g :: FunKind a c -> Type) (x :: a) Source #
Instance details Defined in DeFun.Function type App (CompSym2 f g :: FunKind a c -> Type) (x :: a) = Comp f g x
type App (FlipSym2 f b2 :: FunKind a1 c -> Type) (a2 :: a1) Source #
Instance details Defined in DeFun.Function type App (FlipSym2 f b2 :: FunKind a1 c -> Type) (a2 :: a1) = Flip f b2 a2
type App LAndSym (x :: Bool) Source #
Instance details Defined in DeFun.Bool type App LAndSym (x :: Bool) = LAndSym1 x
type App LOrSym (x :: Bool) Source #
Instance details Defined in DeFun.Bool type App LOrSym (x :: Bool) = LOrSym1 x
type App (ConstSym :: FunKind a (b ~> a) -> Type) (x :: a) Source #
Instance details Defined in DeFun.Function type App (ConstSym :: FunKind a (b ~> a) -> Type) (x :: a) = ConstSym1 x :: FunKind b a -> Type
type App (FoldlSym1 f :: FunKind b ([a] ~> b) -> Type) (z :: b) Source #
Instance details Defined in DeFun.List type App (FoldlSym1 f :: FunKind b ([a] ~> b) -> Type) (z :: b) = FoldlSym2 f z
type App (FoldrSym1 f :: FunKind b ([a] ~> b) -> Type) (z :: b) Source #
Instance details Defined in DeFun.List type App (FoldrSym1 f :: FunKind b ([a] ~> b) -> Type) (z :: b) = FoldrSym2 f z
type App (Con2 f :: FunKind a1 (a2 ~> b) -> Type) (arg :: a1) Source #
Instance details Defined in DeFun.Core type App (Con2 f :: FunKind a1 (a2 ~> b) -> Type) (arg :: a1) = Con1 (f arg)
type App (FlipSym1 f :: FunKind b (a ~> c) -> Type) (x :: b) Source #
Instance details Defined in DeFun.Function type App (FlipSym1 f :: FunKind b (a ~> c) -> Type) (x :: b) = FlipSym2 f x
type App (Con3 f :: FunKind a1 (a2 ~> (b ~> c)) -> Type) (arg :: a1) Source #
Instance details Defined in DeFun.Core type App (Con3 f :: FunKind a1 (a2 ~> (b ~> c)) -> Type) (arg :: a1) = Con2 (f arg)
type App (FoldlSym2 f z :: FunKind [a] b -> Type) (xs :: [a]) Source #
Instance details Defined in DeFun.List type App (FoldlSym2 f z :: FunKind [a] b -> Type) (xs :: [a]) = Foldl f z xs
type App (FoldrSym2 f z :: FunKind [a] b -> Type) (xs :: [a]) Source #
Instance details Defined in DeFun.List type App (FoldrSym2 f z :: FunKind [a] b -> Type) (xs :: [a]) = Foldr f z xs
type App (SequenceSym :: FunKind [[a]] [[a]] -> Type) (xss :: [[a]]) Source #
Instance details Defined in DeFun.List type App (SequenceSym :: FunKind [[a]] [[a]] -> Type) (xss :: [[a]]) = Sequence xss
type App (ConcatSym :: FunKind [[a]] [a] -> Type) (xss :: [[a]]) Source #
Instance details Defined in DeFun.List type App (ConcatSym :: FunKind [[a]] [a] -> Type) (xss :: [[a]]) = Concat xss
type App (ReverseSym :: FunKind [a] [a] -> Type) (xs :: [a]) Source #
Instance details Defined in DeFun.List type App (ReverseSym :: FunKind [a] [a] -> Type) (xs :: [a]) = Reverse xs
type App (AppendSym1 xs :: FunKind [a] [a] -> Type) (ys :: [a]) Source #
Instance details Defined in DeFun.List type App (AppendSym1 xs :: FunKind [a] [a] -> Type) (ys :: [a]) = Append xs ys
type App (FilterSym1 p :: FunKind [a] [a] -> Type) (xs :: [a]) Source #
Instance details Defined in DeFun.List type App (FilterSym1 p :: FunKind [a] [a] -> Type) (xs :: [a]) = Filter p xs
type App (ConcatMapSym1 f :: FunKind [a] [b] -> Type) (xs :: [a]) Source #
Instance details Defined in DeFun.List type App (ConcatMapSym1 f :: FunKind [a] [b] -> Type) (xs :: [a]) = ConcatMap f xs
type App (MapSym1 f :: FunKind [a] [b] -> Type) (xs :: [a]) Source #
Instance details Defined in DeFun.List type App (MapSym1 f :: FunKind [a] [b] -> Type) (xs :: [a]) = Map f xs
type App (Map2Sym2 f xs :: FunKind [b] [c] -> Type) (ys :: [b]) Source #
Instance details Defined in DeFun.List type App (Map2Sym2 f xs :: FunKind [b] [c] -> Type) (ys :: [b]) = Map2 f xs ys
type App (ZipWithSym2 f xs :: FunKind [b] [c] -> Type) (ys :: [b]) Source #
Instance details Defined in DeFun.List type App (ZipWithSym2 f xs :: FunKind [b] [c] -> Type) (ys :: [b]) = ZipWith f xs ys
type App (AppendSym :: FunKind [a] ([a] ~> [a]) -> Type) (xs :: [a]) Source #
Instance details Defined in DeFun.List type App (AppendSym :: FunKind [a] ([a] ~> [a]) -> Type) (xs :: [a]) = AppendSym1 xs
type App (Map2Sym1 f :: FunKind [a] ([b] ~> [c]) -> Type) (xs :: [a]) Source #
Instance details Defined in DeFun.List type App (Map2Sym1 f :: FunKind [a] ([b] ~> [c]) -> Type) (xs :: [a]) = Map2Sym2 f xs
type App (ZipWithSym1 f :: FunKind [a] ([b] ~> [c]) -> Type) (xs :: [a]) Source #
Instance details Defined in DeFun.List type App (ZipWithSym1 f :: FunKind [a] ([b] ~> [c]) -> Type) (xs :: [a]) = ZipWithSym2 f xs
type App (FilterSym :: FunKind (a ~> Bool) ([a] ~> [a]) -> Type) (p :: a ~> Bool) Source #
Instance details Defined in DeFun.List type App (FilterSym :: FunKind (a ~> Bool) ([a] ~> [a]) -> Type) (p :: a ~> Bool) = FilterSym1 p
type App (JoinSym :: FunKind (a ~> (a ~> b)) (a ~> b) -> Type) (f :: a ~> (a ~> b)) Source #
Instance details Defined in DeFun.Function type App (JoinSym :: FunKind (a ~> (a ~> b)) (a ~> b) -> Type) (f :: a ~> (a ~> b)) = JoinSym1 f
type App (FoldrSym :: FunKind (a ~> (b ~> b)) (b ~> ([a] ~> b)) -> Type) (f :: a ~> (b ~> b)) Source #
Instance details Defined in DeFun.List type App (FoldrSym :: FunKind (a ~> (b ~> b)) (b ~> ([a] ~> b)) -> Type) (f :: a ~> (b ~> b)) = FoldrSym1 f
type App (ConcatMapSym :: FunKind (a ~> [b]) ([a] ~> [b]) -> Type) (f :: a ~> [b]) Source #
Instance details Defined in DeFun.List type App (ConcatMapSym :: FunKind (a ~> [b]) ([a] ~> [b]) -> Type) (f :: a ~> [b]) = ConcatMapSym1 f
type App (MapSym :: FunKind (a ~> b) ([a] ~> [b]) -> Type) (f :: a ~> b) Source #
Instance details Defined in DeFun.List type App (MapSym :: FunKind (a ~> b) ([a] ~> [b]) -> Type) (f :: a ~> b) = MapSym1 f
type App (FoldlSym :: FunKind (b ~> (a ~> b)) (b ~> ([a] ~> b)) -> Type) (f :: b ~> (a ~> b)) Source #
Instance details Defined in DeFun.List type App (FoldlSym :: FunKind (b ~> (a ~> b)) (b ~> ([a] ~> b)) -> Type) (f :: b ~> (a ~> b)) = FoldlSym1 f
type App (ApSym :: FunKind (a ~> (b ~> c)) ((a ~> b) ~> (a ~> c)) -> Type) (f :: a ~> (b ~> c)) Source #
Instance details Defined in DeFun.Function type App (ApSym :: FunKind (a ~> (b ~> c)) ((a ~> b) ~> (a ~> c)) -> Type) (f :: a ~> (b ~> c)) = ApSym1 f
type App (Map2Sym :: FunKind (a ~> (b ~> c)) ([a] ~> ([b] ~> [c])) -> Type) (f :: a ~> (b ~> c)) Source #
Instance details Defined in DeFun.List type App (Map2Sym :: FunKind (a ~> (b ~> c)) ([a] ~> ([b] ~> [c])) -> Type) (f :: a ~> (b ~> c)) = Map2Sym1 f
type App (ZipWithSym :: FunKind (a ~> (b ~> c)) ([a] ~> ([b] ~> [c])) -> Type) (f :: a ~> (b ~> c)) Source #
Instance details Defined in DeFun.List type App (ZipWithSym :: FunKind (a ~> (b ~> c)) ([a] ~> ([b] ~> [c])) -> Type) (f :: a ~> (b ~> c)) = ZipWithSym1 f
type App (FlipSym :: FunKind (a ~> (b ~> c)) (b ~> (a ~> c)) -> Type) (f :: a ~> (b ~> c)) Source #
Instance details Defined in DeFun.Function type App (FlipSym :: FunKind (a ~> (b ~> c)) (b ~> (a ~> c)) -> Type) (f :: a ~> (b ~> c)) = FlipSym1 f
type App (CompSym :: FunKind (b ~> c) ((a ~> b) ~> (a ~> c)) -> Type) (f :: b ~> c) Source #
Instance details Defined in DeFun.Function type App (CompSym :: FunKind (b ~> c) ((a ~> b) ~> (a ~> c)) -> Type) (f :: b ~> c) = CompSym1 f :: FunKind (a ~> b) (a ~> c) -> Type
type App (ApSym1 f :: FunKind (a ~> b) (a ~> c) -> Type) (g :: a ~> b) Source #
Instance details Defined in DeFun.Function type App (ApSym1 f :: FunKind (a ~> b) (a ~> c) -> Type) (g :: a ~> b) = ApSym2 f g
type App (CompSym1 f :: FunKind (a ~> b) (a ~> c) -> Type) (g :: a ~> b) Source #
Instance details Defined in DeFun.Function type App (CompSym1 f :: FunKind (a ~> b) (a ~> c) -> Type) (g :: a ~> b) = CompSym2 f g

type (@@) (a1 :: a ~> k) (b :: a) = App a1 b infixl 9 Source #

An infix synonym for App.

Note: there is a term version which is a synonym to appLam.

Lam

newtype Lam (a1 :: a -> Type) (b1 :: b -> Type) (f :: a ~> b) Source #

A term-level representation of defunctionalized type function.

If the a and b type arguments are singletons, then Lam a b itself will be a singleton of the defunctionalized type function, but in general it may not be. (c.f NP Sing is a list singleton, but NP is more general).

Constructors

Lam
Fields appLam :: LamRep a1 b1 f

type (:~>) (a1 :: a -> Type) (b1 :: b -> Type) = Lam a1 b1 infixr 0 Source #

An infix synonym for Lam

mkLam :: forall {a1} {b1} (a2 :: a1 -> Type) (b2 :: b1 -> Type) (f :: a1 ~> b1). LamRep a2 b2 f -> Lam a2 b2 f Source #

A constructor of Lam

type LamRep (a1 :: a -> Type) (b1 :: b -> Type) (fun :: a ~> b) = forall (x :: a). a1 x -> b1 (fun @@ x) Source #

Unwrapped representation of defunctionalized type function.

(@@) :: forall {a1} {k} a2 b (f :: a1 ~> k) (x :: a1). Lam a2 b f -> a2 x -> b (f @@ x) infixl 9 Source #

An infix synonym for appLam.

Note: there is a type version which is a synonym to App.

type Lam2 (a2 :: a -> Type) (b1 :: a1 -> Type) (c :: b -> Type) (fun :: a ~> (a1 ~> b)) = Lam a2 (b1 :~> c) fun Source #

A term-level representation of binary defunctionalized type function.

type Lam3 (a3 :: a -> Type) (b1 :: a1 -> Type) (c :: a2 -> Type) (d :: b -> Type) (fun :: a ~> (a1 ~> (a2 ~> b))) = Lam a3 (b1 :~> (c :~> d)) fun Source #

A term-level representation of ternary defunctionalized type function.

type LamRep2 (a1 :: a -> Type) (b1 :: b -> Type) (c1 :: c -> Type) (fun :: a ~> (b ~> c)) = forall (x :: a) (y :: b). a1 x -> b1 y -> c1 ((fun @@ x) @@ y) Source #

Unwrapped representation of binary defunctionalized type function.

type LamRep3 (a1 :: a -> Type) (b1 :: b -> Type) (c1 :: c -> Type) (d1 :: d -> Type) (fun :: a ~> (b ~> (c ~> d))) = forall (x :: a) (y :: b) (z :: c). a1 x -> b1 y -> c1 z -> d1 (((fun @@ x) @@ y) @@ z) Source #

Unwrapped representation of ternary defunctionalized type function.

pattern Lam2 :: LamRep2 a3 b2 c fun -> Lam2 a3 b2 c fun Source #

Lam2 explicitly bidirectional pattern synonyms for binary defunctionalized type function.

pattern Lam3 :: LamRep3 a4 b2 c d fun -> Lam3 a4 b2 c d fun Source #

Lam3 explicitly bidirectional pattern synonyms for ternary defunctionalized type function.

mkLam2 :: forall {a1} {a2} {b1} (a3 :: a1 -> Type) (b2 :: a2 -> Type) (c :: b1 -> Type) (fun :: a1 ~> (a2 ~> b1)). LamRep2 a3 b2 c fun -> Lam2 a3 b2 c fun Source #

Constructor of Lam2

appLam2 :: forall {a1} {b1} {c1} (a2 :: a1 -> Type) (b2 :: b1 -> Type) (c2 :: c1 -> Type) (fun :: a1 ~> (b1 ~> c1)). Lam2 a2 b2 c2 fun -> LamRep2 a2 b2 c2 fun Source #

Destructor of Lam2

mkLam3 :: forall {a1} {a2} {a3} {b1} (a4 :: a1 -> Type) (b2 :: a2 -> Type) (c :: a3 -> Type) (d :: b1 -> Type) (fun :: a1 ~> (a2 ~> (a3 ~> b1))). LamRep3 a4 b2 c d fun -> Lam3 a4 b2 c d fun Source #

Constructor of Lam3

appLam3 :: forall {a1} {b1} {c1} {d1} (a2 :: a1 -> Type) (b2 :: b1 -> Type) (c2 :: c1 -> Type) (d2 :: d1 -> Type) (fun :: a1 ~> (b1 ~> (c1 ~> d1))). Lam3 a2 b2 c2 d2 fun -> LamRep3 a2 b2 c2 d2 fun Source #

Destructor of Lam3

Con

data Con1 (con :: a -> b) (arg :: FunKind a b) Source #

Wrapper for converting the normal type-level arrow into a ~>. For example, given

>>> data Nat = Z | S Nat

we can write

>>> :kind! Map (Con1 S) '[Z, S Z]
Map (Con1 S) '[Z, S Z] :: [Nat]
= [S Z, S (S Z)]

Instances

Instances details

type App (Con1 f :: FunKind a b -> Type) (x :: a) Source #
Instance details Defined in DeFun.Core type App (Con1 f :: FunKind a b -> Type) (x :: a) = f x

data Con2 (con :: a -> b -> c) (arg :: FunKind a (b ~> c)) Source #

Similar to Con1, but for two-parameter type constructors.

Instances

Instances details

type App (Con2 f :: FunKind a1 (a2 ~> b) -> Type) (arg :: a1) Source #
Instance details Defined in DeFun.Core type App (Con2 f :: FunKind a1 (a2 ~> b) -> Type) (arg :: a1) = Con1 (f arg)

data Con3 (con :: a -> b -> c -> d) (arg :: FunKind a (b ~> (c ~> d))) Source #

Similar to Con2, but for three-parameter type constructors.

Instances

Instances details

type App (Con3 f :: FunKind a1 (a2 ~> (b ~> c)) -> Type) (arg :: a1) Source #
Instance details Defined in DeFun.Core type App (Con3 f :: FunKind a1 (a2 ~> (b ~> c)) -> Type) (arg :: a1) = Con2 (f arg)

con1 :: forall {a1} {b1} (a2 :: a1 -> Type) (b2 :: b1 -> Type) (con :: a1 -> b1). LamRep a2 b2 (Con1 con) -> Lam a2 b2 (Con1 con) Source #

A term-level constructor for Lam of Con1. For example, given

>>> data Nat = Z | S Nat
>>> data SNat (n :: Nat) where { SZ :: SNat Z; SS :: SNat n -> SNat (S n) }
>>> deriving instance Show (SNat n)

we can define

>>> let conS = con1 SS -- taking a singleton(-like) constructor.
>>> :type conS
conS :: Lam SNat SNat (Con1 S)

and use it with term level functions

>>> map conS (SZ :* SS SZ :* SS (SS SZ) :* Nil)
SS SZ :* SS (SS SZ) :* SS (SS (SS SZ)) :* Nil

con2 :: forall {a1} {b1} {c1} (a2 :: a1 -> Type) (b2 :: b1 -> Type) (c2 :: c1 -> Type) (con :: a1 -> b1 -> c1). LamRep2 a2 b2 c2 (Con2 con) -> Lam2 a2 b2 c2 (Con2 con) Source #

A term-level constructor for Lam of Con2

con3 :: forall {a1} {b1} {c1} {d1} (a2 :: a1 -> Type) (b2 :: b1 -> Type) (c2 :: c1 -> Type) (d2 :: d1 -> Type) (con :: a1 -> b1 -> c1 -> d1). LamRep3 a2 b2 c2 d2 (Con3 con) -> Lam3 a2 b2 c2 d2 (Con3 con) Source #

A term-level constructor for Lam of Con2