Safe Haskell	Trustworthy
Language	Haskell2010

DeFun.Core

Contents

FunKind
Fun
App
Lam
Con

Description

Defunctorization core primitives.

Synopsis

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

Documentation

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

FunKind

data FunKind :: Type -> Type -> Type 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 (@@) a b = App a b infixl 9 Source #

An infix synonym for App.

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

Lam

newtype Lam a b f 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 a b f

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

An infix synonym for Lam

mkLam :: LamRep a b f -> Lam a b f Source #

A constructor of Lam

type LamRep a b fun = forall x. a x -> b (fun @@ x) Source #

Unwrapped representation of defunctionalized type function.

(@@) :: Lam a b f -> a 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 a b c fun = Lam a (b :~> c) fun Source #

A term-level representation of binary defunctionalized type function.

type Lam3 a b c d fun = Lam a (b :~> (c :~> d)) fun Source #

A term-level representation of ternary defunctionalized type function.

type LamRep2 a b c fun = forall x y. a x -> b y -> c ((fun @@ x) @@ y) Source #

Unwrapped representation of binary defunctionalized type function.

type LamRep3 a b c d fun = forall x y z. a x -> b y -> c z -> d (((fun @@ x) @@ y) @@ z) Source #

Unwrapped representation of ternary defunctionalized type function.

pattern Lam2 :: LamRep2 a b c fun -> Lam2 a b c fun Source #

Lam2 explicitly bidirectional pattern synonyms for binary defunctionalized type function.

pattern Lam3 :: LamRep3 a b c d fun -> Lam3 a b c d fun Source #

Lam3 explicitly bidirectional pattern synonyms for ternary defunctionalized type function.

mkLam2 :: LamRep2 a b c fun -> Lam2 a b c fun Source #

Constructor of Lam2

appLam2 :: Lam2 a b c fun -> LamRep2 a b c fun Source #

Destructor of Lam2

mkLam3 :: LamRep3 a b c d fun -> Lam3 a b c d fun Source #

Constructor of Lam3

appLam3 :: Lam3 a b c d fun -> LamRep3 a b c d fun Source #

Destructor of Lam3

Con

data Con1 con arg 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 arg 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 arg 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 :: LamRep a b (Con1 con) -> Lam a b (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 :: LamRep2 a b c (Con2 con) -> Lam2 a b c (Con2 con) Source #

A term-level constructor for Lam of Con2

con3 :: LamRep3 a b c d (Con3 con) -> Lam3 a b c d (Con3 con) Source #

A term-level constructor for Lam of Con2