Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
In this module we define Church-encoded type-level natural numbers, Church-encoded vectors and Scott-encoded vectors.
See docsfomegagadtsScottVec.agda
for how Scott-encoded vectors work.
Synopsis
- natK ∷ Kind ()
- getEta ∷ Type TyName uni () → Quote (Type TyName uni ())
- zeroT ∷ Type TyName uni ()
- succT ∷ Type TyName uni ()
- plusT ∷ Type TyName uni ()
- getStepFun ∷ TyName → Type TyName uni () → TyName → Quote (Type TyName uni ())
- churchVec ∷ Type TyName uni ()
- churchNil ∷ Term TyName Name uni fun ()
- churchCons ∷ Term TyName Name uni fun ()
- churchConcat ∷ Term TyName Name uni fun ()
- scottVecF ∷ Type TyName uni ()
- scottVec ∷ Type TyName uni ()
- scottNil ∷ Term TyName Name uni fun ()
- scottCons ∷ Term TyName Name uni fun ()
- scottHead ∷ uni `HasTypeAndTermLevel` () ⇒ Term TyName Name uni fun ()
- scottSumHeadsOr0 ∷ (uni `HasTypeAndTermLevel` Integer, uni `HasTypeAndTermLevel` ()) ⇒ Term TyName Name uni DefaultFun ()
Documentation
getEta ∷ Type TyName uni () → Quote (Type TyName uni ()) Source #
getEta n = \(f :: * -> *) (z :: *) -> n f z
plusT ∷ Type TyName uni () Source #
plusT = \(n : natK) (m : natK) (f :: * -> *) (z :: *) -> n f (m f z)
getStepFun ∷ TyName → Type TyName uni () → TyName → Quote (Type TyName uni ()) Source #
stepFun a r1 r2 = all (p :: natK). a -> r1 p -> r2 (succT p)
churchVec ∷ Type TyName uni () Source #
churchVec = \(a :: *) (n :: natK) -> all (r :: natK -> *). (all (p :: natK). a -> r p -> r (succT p)) -> r zeroT -> r n
churchNil ∷ Term TyName Name uni fun () Source #
churchNil = /\(a :: *) -> /\(r :: natK -> *) -> \(f : all (p :: natK). a -> r p -> r (succT p)) (z : r zeroT) -> z
churchCons ∷ Term TyName Name uni fun () Source #
churchCons = /\(a :: *) (n :: natK) -> \(x : a) (xs : churchVec a n) -> /\(r :: natK -> *) -> \(f : all (p :: natK). a -> r p -> r (succT p)) (z : r zeroT) -> f {n} x (xs {r} f z)
churchConcat ∷ Term TyName Name uni fun () Source #
churchConcat = /\(a :: *) (n :: natK) (m :: natK) -> \(xs : churchVec a n) (ys : churchVec a m) -> /\(r :: natK -> *) -> \(f : all (p :: natK). a -> r p -> r (succT p)) (z : r zeroT) -> xs {\(p :: natK) -> r (plusT p m)} (/\(p :: natK) -> f {plusT p m}) (ys {r} f z)
scottVecF ∷ Type TyName uni () Source #
scottVecF = \(a :: *) (rec :: natK -> *) (n :: natK) -> all (r :: natK -> *). (all (p :: natK). a -> rec p -> r (succT p)) -> r zeroT -> r n
scottNil ∷ Term TyName Name uni fun () Source #
scottNil = /\(a :: *) -> iwrap (scottVecF a) zeroT (/\(r :: natK -> *) -> \(f : all (p :: natK). a -> scottVec a p -> r (succT p)) (z : r zeroT) -> z)
scottCons ∷ Term TyName Name uni fun () Source #
scottCons = /\(a :: *) (n :: natK) -> \(x : a) (xs : scottVec a n) -> iwrap (scottVecF a) (succT n) (/\(r :: natK -> *) -> \(f : all (p :: natK). a -> scottVec a p -> r (succT p)) (z : r zeroT) -> f {n} x xs)
scottHead ∷ uni `HasTypeAndTermLevel` () ⇒ Term TyName Name uni fun () Source #
scottHead = /\(a :: *) (n :: natK) -> (xs : scottVec a (suc n)) -> unwrap xs {\(p :: natK) -> p (\(z :: *) -> a) unit} (/\(p :: natK) (x : a) (xs' : scottVec a p) -> x) unitval
scottSumHeadsOr0 ∷ (uni `HasTypeAndTermLevel` Integer, uni `HasTypeAndTermLevel` ()) ⇒ Term TyName Name uni DefaultFun () Source #
scottSumHeadsOr0 = /\(n :: natK) -> (xs ys : scottVec integer n) -> unwrap xs {\(p :: natK) -> (scottVec Integer n -> scottVec integer p) -> integer} (/\(p :: natK) (x : integer) (xs' : scottVec integer p) \(coe : scottVec Integer n -> scottVec integer (suc p)) -> x + scottHead {integer} {p} (coe ys)) (\(coe : scottVec Integer n -> scottVec integer zero) -> 0) (/\(xs' :: scottVec Integer n) -> xs')