| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
PlutusCore.Examples.Data.Shad
Synopsis
- shad :: uni `Includes` Integer => Type TyName uni ()
- mkShad :: uni `Includes` Integer => Term TyName Name uni fun ()
- recUnit :: uni `Includes` () => Type TyName uni ()
- runRecUnit :: uni `Includes` () => Term TyName Name uni fun ()
Documentation
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.
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.