[TYPES] a naive question on datatype declarations

[Andreas Rossberg]

From the last paragraph of your question it sounds as if you particularly wonder how to represent the nominal typing aspect of datatype declarations, i.e., the fact that structurally identical type definitions are still considered distinct.

Probably the simplest way to represent nominal types is to model them as abstract data types, which in turn can be understood as existential type, e.g., per Mitchell & Plotkins seminal paper [1].

Using that idea, a nominal datatype declaration like

    data Bool = True | False
    …rest of program…    

can be see as a binding unpacking an existential:

    unpack ⟨𝑏𝑜𝑜𝑙, ⟨𝑡𝑟𝑢𝑒, 𝑓𝑎𝑙𝑠𝑒, 𝑐𝑎𝑠𝑒𝑏𝑜𝑜𝑙⟩⟩ = 𝑏𝑜𝑜𝑙𝑖𝑚𝑝𝑙 in
    …rest of program…

where 𝑏𝑜𝑜𝑙𝑖𝑚𝑝𝑙 is the following existential package:

    pack ⟨1 + 1, ⟨inl ⟨⟩, inr ⟨⟩, Λα. λ𝑏:(1+1). λ𝑓:(1→α). λ𝑔:(1→α). case 𝑏 of inl 𝑥 ⇒ 𝑓 𝑥 | inr 𝑦 ⇒ 𝑔 𝑦⟩⟩ as 𝐵𝑜𝑜𝑙

and 𝐵𝑜𝑜𝑙 is the type

    ∃𝑏𝑜𝑜𝑙. 𝑏𝑜𝑜𝑙 × 𝑏𝑜𝑜𝑙 × (∀α. 𝑏𝑜𝑜𝑙 → (1 → α) → (1 → α) → α)

The first two values of this ADT signature are the Bool constructors, and the last encapsulates case analysis, as e.g. needed for compiling pattern matching.

Similarly, List would be represented as the higher-kinded existential

    ∃𝑙𝑖𝑠𝑡:(* → *). (∀α. 𝑙𝑖𝑠𝑡 α) × (∀α. α → 𝑙𝑖𝑠𝑡 α → 𝑙𝑖𝑠𝑡 α) × (∀α. ∀β. 𝑙𝑖𝑠𝑡 α → (1 → β) → (α → 𝑙𝑖𝑠𝑡 α → β) → β)

Because each type definition is represented by a separate unpack expression that binds a separate type variable in this scheme, multiple definitions are always viewed as distinct types in the rest of the program.

A variation of this encoding was e.g. used in Harper & Stone’s type-theoretic model of Standard ML [2], although they take a detour through a more powerful module calculus, which isn’t needed for the basic encoding.

/Andreas


[1] John Mitchell, Gordon Plotkin. Abstract Types Have Existential Type. in: TOPLAS 10(3), 1988.

[2] Robert Harper, Christopher Stone. A Type-Theoretic Interpretation of Standard ML. in: Proof, Language, and Interaction: Essays in Honour of Robin Milner, 2000.



> On 26. Jan 2024, at 23:18, Gershom B <gershomb at gmail.com> wrote:
> 
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> In typical treatments of languages with recursive types, we present a
> syntax with either isorecursive or equirecursive types. But we do not
> have a syntax for introduction of type declarations.
> 
> This is to say that we assemble types out of constructors for e.g.,
> polymorphism, recursion, sum, product, unit, exponential (give or
> take).
> 
> But we do not have the equivalent of a "data" declaration in Haskell
> that lets us explicitly say
> 
> data Bool = True | False
> 
> or
> 
> data List a = Nil | Cons a
> 
> It is, I suppose, expected that readers of these papers can think
> through how to translate any given data datatypes in languages with
> explicit declaration into the underlying fixed type calculus.
> 
> However, I am curious if there is any reference for *explicit*
> treatment of the syntax for datatype declarations and semantic
> modeling of such?
> 
> One reason for such would be that in the calculi I described above,
> there's of course no way to distinguish between the above `data Bool`
> and e.g. `1 + 1`, while it might be desirable to maintain that strict
> distinction between actual equality and merely observable isomorphism.
> 
> Thanks,
> Gershom