search

pre-srfi / static-scheme

11 stars 0 forks source link

Possible type annotation #10

Open mnieper opened 3 years ago

mnieper commented 3 years ago

There are conservative extensions to the HM system, meaning that every program that is correct according to HM will also typecheck in such an extension (without any type annotations).

Some such extensions that are attractive due to their expressiveness would, however, need some type annotations (e.g. for polymorphic arguments to lambda). Moreover, when calling Scheme procedures through the "FFI" interface, we need to supply types.

Therefore, we should also think about how to denote types Scheme-like. For example, type functions (like Haskell's [.]) should preferrably live in the same unique namespace as every other identifier of Scheme (like those denoting keywords and variables) and should be lexically scoped as well. (This would also play well with established Scheme macro systems.)

The syntax for type annotations isn't obvious. A syntax as the following one (for explicit annotations for whatever reason) doesn't seem to be a good one, for example:

(lambda (x : T) <body>)

The reason is, of course, that it could also denote a function of the three arguments x, :, and T.

aijony commented 3 years ago

I think for special cases like define, lambda, let, etc. (x : T) isn't the worst choice if all we are missing out on are local variables being named :. But what would multiple type-signature arguments look like? (lambda (x : T y : Z) <body>) is hard to read as a human.

Some other choices could be: (lambda ((the T x)) <body>), (lambda ((: x T)) <body>), (lambda ((x : T)) <body>). I am partial to the last one, or the second one with SRFI-105 (i.e. (lambda ({x : t}) <body>)).

We could also have the option to annotate the lambda (not let or define) externally:

(the (-> T H) (lambda (x) <body>))

We could also take these forms:

(define x : T)
(define f
  (lambda (x) : (-> T H)
   <body>))
(define (f x) : (-> T H)
   <body>)

And for top-level bindings should we have a separate type annotation?

(assert x T)
(define x t)

A lot of these aren't mutually exclusive either.

lassik commented 3 years ago

Strongly recommend (the <type-signature> <value>). If you put the annotation in one place where you use a variable, you create a constraint for the inference engine and it ought to be able to figure out how to use the same type for that variable everywhere else as well. So you don't have to annotate function arguments in the arg list, you can annotate them in the function body.

lassik commented 3 years ago

However, for FFI (i.e. dynamic Scheme) procedures, a full annotation is needed.

lassik commented 3 years ago

Of course, lots of functional programmers are very type-happy and deliberately want to write out a full annotation for every top-level function. (Yes, we still have to figure out what "top level" means for us.)

lassik commented 3 years ago

It comes back to the cultural difference about whether types are an invisible correctness tool like GC, or something to admire in themselves.

mnieper commented 3 years ago

It would be rather "unschemy" to give the identifier : a special status in argument lists. So far it has been guaranteed that lambda can bind any identifier regardless of its earlier binding. This property shouldn't be destroyed lightly.

There is a similar issue with syntax like

(assert x T)
(define x t)

In ordinary Scheme, a binding construct like define creates a fresh binding so the semantics of an assert coming earlier is quite unclear. We should keep in mind that x might have bound to a syntax keyword, for example.

Whether annotating arguments of lambdas or annotating the full lambda is better/necessary may also depend on the type system.

If possible I would love to see a system that works uniformly across Scheme's binding constructs for variables, amongst which we have lambda, let, named let, etc.

PS Curly braces (which I don't like much, but this is my personal opinion) could only be optional as the usual Scheme reader should be able to read Steme code. Likewise, Scheme macros should be applicable to Steme syntax.

lassik commented 3 years ago

I would love to see a system that works uniformly across Scheme's binding constructs for variables, amongst which we have lambda, let, named let, etc.

In the usual HM fare, let doesn't need annotations because an initial value must be assigned, and the type can be inferred from that value. Same goes for named let and let-values as well as (define foo ...) and define-values.

lambda and (define (f ...) ...) are not as easy.

aijony commented 3 years ago

It comes back to the cultural difference about whether types are an invisible correctness tool like GC, or something to admire in themselves.

It also depends if you want Steme to have a narrow focus that only does HM with tightly moving parts or is a framework that can be expanded upon with modular components. Both have their own advantages. It's the diamond vs. the ball of mud.

If you are going with the well-designed HM only approach, I would not have type annotations.

If Steme is meant to have extensions (like higher-rank types #9), then you should have (edit: optional) type annotations even for the HM only base.

mnieper commented 3 years ago

What do you mean by "should have type annotations even for the HM only base"? Shouldn't they be optional in any case?

aijony commented 3 years ago

What do you mean by "should have type annotations even for the HM only base"? Shouldn't they be optional in any case?

Yes, I mean you "should have (optional) type annotations even for the HM only base", my bad.