Safe Haskell	Safe-Inferred
Language	Haskell2010

PlutusCore.Examples.Data.Vec

Description

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

natK ∷ Kind () Source #

natK = (* -> *) -> * -> *

getEta ∷ Type TyName uni () → Quote (Type TyName uni ()) Source #

getEta n = \(f :: * -> *) (z :: *) -> n f z

zeroT ∷ Type TyName uni () Source #

zeroT = \(f :: * -> *) (z :: *) -> z

succT ∷ Type TyName uni () Source #

succT = \(n : natK) (f :: * -> *) (z :: *) -> f (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

scottVec ∷ Type TyName uni () Source #

scottVec = \(a :: *) (n :: natK) -> ifix (scottVecF a) 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')