Although it is true that types are not preserved for open terms, they should be preserved for closed terms.
E.g. in the thunking transformation
let nonstrict x = <x_rhs> in
<term>
becomes
let strict x = \() -> <x_rhs> in
<term'>
So the rhs gets a different type and the occurrences of x in get a different type.
However, any occurence x is replaced by x (), so these expressions stay of the same type.
When type-checking, the environment Γ is different (see also next subsection). But, I think
that any closed term must preserve the type exactly.
Is the definition of static semantics good enough?
Definition 5.2 roughly states that:
if R(t, t') then
Δ ; Γ ⊢ t : τ
implies
Δ'; Γ' ⊢ t' : τ'
where
R_delta(Δ, Δ')
R_gamma(Γ, Γ')
R_ty(τ, τ')
(where R_... are appropriate relations for the translation relation R)
Now consider this program:
let strict x : Int = <x_rhs> in
let nonstrict y : Int = <y_rhs> in
<term>
in , Γ looks like
Γ = [x ↦ Int, y ↦ Int]
and after the thunking transformation it looks like
Γ = [x ↦ Int, y ↦ () -> Int]
The problem is that R_gamma cannot distinguish the types of x and y in Γ: there is no information in Γ about which variable is bound strict or lazy.
The case of datatype encodings might be trickier. Although the same principle applies as the thunking transformation, since ADTs are similarly let-bound, datatypes may 'escape' their scope:
Open vs closed terms
Although it is true that types are not preserved for open terms, they should be preserved for closed terms.
E.g. in the thunking transformation
becomes
So the rhs gets a different type and the occurrences of x in get a different type.
However, any occurence
x
is replaced byx ()
, so these expressions stay of the same type.When type-checking, the environment Γ is different (see also next subsection). But, I think that any closed term must preserve the type exactly.
Is the definition of static semantics good enough?
Definition 5.2 roughly states that:
if R(t, t') then Δ ; Γ ⊢ t : τ implies Δ'; Γ' ⊢ t' : τ'
where R_delta(Δ, Δ') R_gamma(Γ, Γ') R_ty(τ, τ')
(where R_... are appropriate relations for the translation relation R)
Now consider this program:
in, Γ looks like
and after the thunking transformation it looks like
The problem is that R_gamma cannot distinguish the types of x and y in Γ: there is no information in Γ about which variable is bound strict or lazy.
The case of datatype encodings might be trickier. Although the same principle applies as the thunking transformation, since ADTs are similarly let-bound, datatypes may 'escape' their scope: