plutus-core-0.1.0.0: Language library for Plutus Core

Synopsis

# Documentation

shad :: uni Includes Integer => Type TyName uni () Source #

\(a :: *) -> ifix (getShadF a) a

mkShad :: uni Includes Integer => Term TyName Name uni fun () Source #

Test that shadowing does not result in variable capture. The definition is as follows:

/\(a :: *) -> wrap (getShadF a) a (\(x : a) -> /\(f :: * -> *) -> \(y : f i) -> 0)

Type checking this term we eventually reach

NORM (vPat (\(a :: k) -> ifix vPat a) arg)

(where in our case vPat is shadF and arg is a), which, if we were naive, would unfold into

a -> all (a :: * -> *). a a -> integer

i.e. we substituted the outer a for i, but due to variable capture via all that outer a now became an inner one, which would be a bug.

But that problem is already solved before type checking starts as we rename the program and that makes all binders uniques, so no variable capture is possible due to the outer and inner bindings being distinct.

recUnit :: uni Includes () => Type TyName uni () Source #

ifix recUnitF ()

runRecUnit :: uni Includes () => Term TyName Name uni fun () Source #

Test that a binder in a pattern functor does not get duplicated. The definition is as follows:

/\(a :: *) -> \(ru : recUnit) -> unwrap ru {a} ru

Type checking this term we eventually reach

NORM (vPat (\(a :: k) -> ifix vPat a) arg)

(where in our case vPat is recUnitF and arg is ()), which, if we were naive, would unfold into

all (r :: *). ifix (\(rec :: * -> *) (i :: *) -> all (r :: *). rec i -> r -> r) () -> r -> r

and break global uniqueness as the all (r :: *) binder appears twice.

But this doesn't happen in the actual code, since when a variable gets looked up during type normalization, its value gets renamed, which means that a fresh variable will be generated for the inner binder and there will be no shadowing.