Toward An Abstract Syntax
I continue to noodle around with an abstract syntax for types in my internal language. (Sigh. This is taking forever.) Here's what I'm looking at now:
τ ::= α | ν⟨σ⟩ | λ(σ)
σ ::= ∀δ,σ | ∃α,σ | τ,σ | ϵ
δ ::= α | α = τ | α > τ
Explanation. A type (τ) is either a named type variable (α), or a channel type of shape (σ) with either λ- or ν- binding. A shape (σ) is a list of universal quantifications, existential quantifications and type declarations terminated by the shape terminator code (ϵ), i.e. a channel that carries no types or values has type ϵ. The universal quantification is enriched with flexible (>) and rigid (=) constraints.
Some syntactic sugar is useful. The trailing ϵ in a shape can be elided from the bracketed expression in a λ- or ν- type expression, i.e. ν⟨α,β,ε⟩ can be written ν⟨α,β⟩. If the shape of a channel type expression has only one term before the ε, then the brackets/parentheses may be elided, i.e. λ(α,ε) can be written λα.
I'm still going back and forth with myself over where the λ's and ν's belong.
My Groups
-
Writers Hub Updated: 59 minutes ago
-
Amnesty International Updated: Yesterday
Neighborhood
Explore friends, family, friends & family, or entire neighborhood.
