Questions regarding the "Design and Implementation" paper

[DAY]

Hi,

I am reading "Design and Implementation" paper.  I have two questions.

1. Is it necessary to have `let' in the core language?  It seems to me in such a rich type system we can introduce it as usual a syntactic sugar of function application.  Of course, it may cause efficiency problems.  Is this the main reason to have it built in?  Or are there other reasons I missed.

2. Among the premises of the typing rules for `let', `S' (the type of the definition) and `T' (the type of the body) both are checked to have type `Type_n'.  Isn't this a restriction?  It seems to me now I could not write something like the following (a silly example, but it shows the restriction):

let x = O in Nat    (because (O : Nat) : Type_0 whereas (Nat : Type_0) : Type_1)

or

let X = Nat in O    (because (Nat : Type_0) : Type_1 whereas (O : Nat) : Type_0)

Is this intended?  If it is, why?  Or I missed something?

Best,

DAY

[Edwin Brady]

Hi there,
Sorry to be slow to reply. Busy few weeks at the minute…

On 3 Mar 2013, at 13:31, DAY <plm...@gmail.com> wrote:

> 1. Is it necessary to have `let' in the core language? It seems to me in such a rich type system we can introduce it as usual a syntactic sugar of function application. Of course, it may cause efficiency problems. Is this the main reason to have it built in? Or are there other reasons I missed.

It isn't strictly necessary, especially since the high level let isn't even implemented with it (at least, not the destructuring form). I do find it convenient though, especially since it makes it possible to cache intermediate results.

> 2. Among the premises of the typing rules for `let', `S' (the type of the definition) and `T' (the type of the body) both are checked to have type `Type_n'. Isn't this a restriction? It seems to me now I could not write something like the following (a silly example, but it shows the restriction):
>
> let x = O in Nat (because (O : Nat) : Type_0 whereas (Nat : Type_0) : Type_1)
>
> or
>
> let X = Nat in O (because (Nat : Type_0) : Type_1 whereas (O : Nat) : Type_0)
>
> Is this intended? If it is, why? Or I missed something?

Hmm. No, it isn't. And the implementation doesn't implement this restriction in any case. Thanks for pointing it out!

Edwin.


--
The University of St Andrews is a charity registered in Scotland : No SC013532

[DAY]

Hi,

Thanks for the answer.

On Saturday, March 9, 2013 5:10:37 PM UTC+1, Edwin Brady wrote:

Hi there,
Sorry to be slow to reply. Busy few weeks at the minute…

On 3 Mar 2013, at 13:31, DAY <plm...@gmail.com> wrote:

> 1. Is it necessary to have `let' in the core language?  It seems to me in such a rich type system we can introduce it as usual a syntactic sugar of function application.  Of course, it may cause efficiency problems.  Is this the main reason to have it built in?  Or are there other reasons I missed.

It isn't strictly necessary, especially since the high level let isn't even implemented with it (at least, not the destructuring form). I do find it convenient though, especially since it makes it possible to cache intermediate results.

What do you mean by "high-level let"?