Re: [TYPES] a naive question on datatype declarations

Sat, 27 Jan 2024 07:23:53 -0800 

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

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 <gersh...@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

Reply via email to