Skip to content

Instantly share code, notes, and snippets.

@MaiaVictor MaiaVictor/eacc.hs
Created Jul 18, 2018

Embed
What would you like to do?
EACC details
-- EACC is obtained from CC by restricting functions to be affine and adding 3 constructs:
-- - Put: `|x` marks a term without free affine variables.
-- - Exp: `!x` is the type of `|x`.
-- - Dup: `$v x y` replaces occurrences of `v` by `x` in `y`.
-- With the following reduction rules:
-- - nf(!a) => !nf(a)
-- - nf(|a) => nf(a)
-- - nf($x y z) => nf(z[y/x])
-- With the following typing rules:
-- - Γ |- x : t Γ |- t : * Γ |- x : !t Γ, x0 : t, ... xN : t |- y : u
-- - ------------ ----------- --------------------------------------------
-- - Γ |- |x : !t Γ |- !t : * Γ |- $v x y : u
--
-- Examples:
-- (Note: I use `:->=` for clarity, but those characters are ignored.)
--
-- The type of Church nats is as expected, except for additional `!`s:
Nat = P : * -> !(P -> P) -> !(P -> P)
-- The number 3 is represented as:
c3 =
Λ P : * ->
λ s : !(P -> P) ->
$ S = s
| λ z : P ->
S (S (S z))
-- Notice that:
-- 1. `Λ` represents an erased lambda. Its variables are not affine.
-- 2. The first `!` was used to allow the duplication of `s`.
-- 3. `$ S = s in ...` was used to duplicate the `s` variable.
-- 4. There is no free affine variable inside the expression inside `|`.
-- 5. There is exactly one `|` between the declaration of S and its occurrences.
-- 6. The term correctly type-checks as `∀ P : * -> !(P -> P) -> !(P -> P)`.
-- 7. If you erase the `!`s, `|`s and `$`s, you get the usual CC definition.
--
-- The definitions of `add`, `mul` and `exp` are as follows:
exp =
λ a : Nat ->
λ b : !Nat ->
Λ P : * ->
$ B = b
a !(P -> P) |(B P)
mul =
λ a : Nat ->
λ b : Nat ->
Λ P : * ->
λ s : !(P -> P) ->
a P (b P s)
add =
λ a : Nat ->
λ b : Nat ->
Λ P : * ->
λ s : ! (P -> P) ->
$ S = s
$ f = (a P |S)
$ g = (b P |S)
| λ z : P ->
f (g z)
-- Notice that all those functions correctly type check as `Nat -> Nat -> Nat`.
-- Notice also that, again, erasing `!`s, `|`s and `$`s gives the usual CC definitions.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.