You'll need to interpret this for me. What language are you working in here?
What is ":=" ? (In Twelf, I've seen ":". In BNF, "::=". In Haskell, ":" and "=".)
Ben : my own ...
Mentioned https://en.wikipedia.org/wiki/Sequent_calculus as something Ben is interested in, in terms of what sorts of programming language paradigms it would be consistent with (if I'm understanding correctly).
Also discussed a bit of (inl) and (inr) in haskell and these contexts, poly type forms in these declarations and definitions, when they're needed and what the syntax is ... and perhaps a bit of why ... haskell inl
s : All(r) All(a) All(b) (r -> a -> b) -> (r -> a) -> r -> b
s := Lam(r) Lam(a) Lam(b)
lam(f : r -> a -> b) lam(g : r -> a) lam(x : r) f x (g x)
k : All(r) All(a) a -> r -> a
k := Lam(r) Lam(a) lam(x : a) lam(y : r) x
bool := All(a) a -> a -> a
true := Lam(a) lam(x : a) lam(y : a) x
false := Lam(a) lam(x : a) lam(y : a) y
if : All(a) bool -> a -> a -> a
if := Lam(a) lam(b : bool) b[a]
We represent a value of an inductive type mu(t.τ) by the recursor it gives.
Rule (15.8b) says that for any τ' and function [τ'/t]τ -> τ' (technically,
the syntax asks for the body of such a function), we may get a τ'. Replacing
the metavariable τ' with the type variable t', we get
mu(t.τ) := All(t') ([t'/t]τ -> t') -> t'. By the nature of the encoding, the
elimination form is just specialization and function application. The
introduction form is:
fold : [mu(t.τ)/t]τ -> mu(t.τ)
fold := lam(u : [mu(t.τ)/t]τ) Lam(t') lam(r : [t'/t]τ -> t')
r map+{t.τ}(x.x[t'] r)(u)
This essentially takes some unfolded u and supplies a recursor whose
behavior, given a "one step of recursion" function r, is to first recurse on
the recursive occurrences in u and then perform the final step with r.
t list := All(t') (t -> t' -> t') -> t' -> t'
I am probably supposed to use parametricity to establish the property it asks for, but I don't think I really follow what the parametricity property would be for this type---it doesn't really explain the pattern.
Note that the definitions in 17.3 involve the introduction of variables u and
x. We assume that these new variables are meant to be chosen to be distinct
from anything free in ρ, e, etc, since the definitions would otherwise not
really make sense. We will use this same implicit assumption in what follows.
In this implementation of existential types, rules (17.1b) and (17.1c) become:
Δ |- ρ type Δ, t type |- τ type Δ Γ |- e : [ρ/t]τ
-------------------------------------------------------------------------
Δ Γ |- Lam(u) lam(x : All(t) τ -> u) x[ρ] e : All(u) (All(t) τ -> u) -> u
Δ Γ |- e_1 : All(u) (All(t) τ -> u) -> u Δ, t type Γ, x : τ |- e_2 : τ_2 Δ |- τ_2 type
--------------------------------------------------------------------------------------------
Δ Γ |- e_1[τ_2] (Lam(t) lam(x : τ) e_2) : τ_2
These are both easily admissible.
For the lazy dynamics, rules (17.2) become:
----------------------------------------
Lam(u) lam(x : All(t) τ -> u) x[ρ] e val
e_1 |-> e_1'
----------------------------------------------------------------------------
e_1[τ_2] (Lam(t) lam(x : τ) e_2) |-> e_1'[τ_2] (Lam(t) lam(x : τ) e_2) : τ_2
------------------------------------------------------------------------------------
(Lam(u) lam(y : All(t) τ -> u) y[ρ] e)[τ_2] (Lam(t) lam(x : τ) e_2) |-> [ρ,e/t,x]e_2
The first two of these are also easily admissible. The third is in fact not
admissible, but it does become admissible if we replace the |-> in the
conclusion with |->*, by the following reduction steps (noting that some
substitutions have no effect by the freshness assumptions):
(Lam(u) lam(y : All(t) τ -> u) y[ρ] e)[τ_2] (Lam(t) lam(x : τ) e_2) |->
(lam(y : All(t) τ -> τ_2) y[ρ] e) (Lam(t) lam(x : τ) e_2) |->
(Lam(t) lam(x : τ) e_2)[ρ] e |->
(lam(x : [ρ/t]τ) [ρ/t]e_2) e |->
[e/x][ρ/t]e_2 = [ρ,e/t,x]e_2
The final equality holds because t cannot be free in e if the terms are
well-typed and x cannot be free in ρ since types cannot contain term
variables.
A value of a coinductive type is a gen expression, which contains a value (or
expression, in the lazy dynamics) of some state type and an operation to
produce one "layer" of unfolding from any given state. The "some" in "some
state type" is precisely captured by existential types, and we can define
nu(t.τ) := Some(t') (t' -> [t'/t]τ) * t'.
The introduction form is essentially just pairing and pack, as should be
expected:
gen{t.τ}(x.e_1; e_2) := pack τ_2 with (lam(x : τ_2) e_1, e_2) as nu(t.τ)
The elimination form is:
unfold{t.τ}(e) := open e as t' with p : (t' -> [t'/t]τ) * t' in
map+{t.τ}(s.gen{t.τ}(s'.p.l s'; s))(p.l p.r)
This unpacks the value for long enough to apply the unfolding function to the current state, and then maps over the result in order to re-pack the new states produced along with the unfolding function.
queue_impl :: (T -> T) -> T
queue_impl := lam(q :: T -> T) <emp : All(t :: T) q[t], ...>
queue :: T
queue := Some(q :: T -> T) queue_impl[q]
list :: T -> T
nil : All(t :: T) list[t]
list := lam(t :: T) mu(l.void + t * l)
nil := ...
simple_queue_impl : queue_impl[list]
simple_queue : queue
simple_queue_impl := <emp := Lam(t :: T) nil[t], ...>
simple_queue := pack list with simple_queue_impl as queue
fancy_queue_struct :: T -> T
fancy_queue_impl : queue_impl[fancy_queue_struct]
fancy_queue : queue
fancy_queue_struct := lam(t :: T) list[t] * list[t]
fancy_queue_impl := <emp := Lam(t :: T) (nil[t], nil[t]), ...>
fancy_queue := pack fancy_queue_struct with fancy_queue_impl as queue
I'm not 100% sure what they're getting at about "both implementations
hav[ing] this type", but certainly typechecking either relies on the facts that
queue_impl[list] and queue_impl[fancy_queue_struct] are not actual
respectively equal-as-terms (even after expanding the meta-level constant
definitions I've done here) to the types that can be assigned to
simple_queue_impl and fancy_queue_impl without use of rule (18.4)---only
"definitionally equal" according to the constructor dynamics.
...