plutus-core
Safe HaskellNone
LanguageHaskell2010

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

Documentation

natK :: Kind () Source #

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

getEta :: forall (uni :: Type -> Type). Type TyName uni () -> Quote (Type TyName uni ()) Source #

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

zeroT :: forall (uni :: Type -> Type). Type TyName uni () Source #

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

succT :: forall (uni :: Type -> Type). Type TyName uni () Source #

succT = \(n : natK) (f :: * -> *) (z :: *) -> f (n f z)

plusT :: forall (uni :: Type -> Type). Type TyName uni () Source #

plusT = \(n : natK) (m : natK) (f :: * -> *) (z :: *) -> n f (m f z)

getStepFun :: forall (uni :: Type -> Type). TyName -> Type TyName uni () -> TyName -> Quote (Type TyName uni ()) Source #

stepFun a r1 r2 = all (p :: natK). a -> r1 p -> r2 (succT p)

churchVec :: forall (uni :: Type -> Type). 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 :: forall (uni :: Type -> Type) fun. 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 :: forall (uni :: Type -> Type) fun. 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 :: forall (uni :: Type -> Type) fun. 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 :: forall (uni :: Type -> Type). 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 :: forall (uni :: Type -> Type). Type TyName uni () Source #

scottVec = \(a :: *) (n :: natK) -> ifix (scottVecF a) n

scottNil :: forall (uni :: Type -> Type) fun. 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 :: forall (uni :: Type -> Type) fun. 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 :: forall (uni :: Type -> Type) fun. HasTypeAndTermLevel uni () => 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 :: forall (uni :: Type -> Type). (HasTypeAndTermLevel uni Integer, HasTypeAndTermLevel uni ()) => 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')