best way to specify static typing?

I have a project that is currently built in a Scheme variant.  Going
forward I'm planning add to it a small run-time compiler, written in
Scheme and C, that will compile some small Domain Specific Language
(DSL) to machine code, ie a JIT.

At the moment, this DSL just needs vectors, basic integers, and
functions and probably mutliple return values and floats.

I'm not interested in designing some language or syntax. I just want to
get the thing compiling and running. I am hoping to model the DSL on
some subset of Scheme.  This seems, to me, to be the simplest, and the
most flexible.

But, the reason I'm doing this is for performance, and so for that
reason, and the ease of writing the compiler, I'm planning to add
static typing to the DSL. And, no, no type inference now.


So, my question is, what's the best way of adding static typing to a
subset of the Scheme syntax?

Common Lisp uses (declare), but that's so wordy, and it puts the type
declarations a bit away from the variable declarations.   And how to
handle type inside a (let) statement?


Here are the ideas I've had so far:

(defun myFunc (x y)
(declare-types \i \i -> \i \i)
;; \i means integer, this function takes two integers and returns
two integers.
..)


or

(let ((x 4 \i) ;;<- the type specifier comes after
(y (foo) \v))
..)


I like the above because they could be easily reconcilable with normal
Scheme, so the addition of some macros could make my DSL code run
interpreted in the Scheme environment.


But, I've toyed with some other ideas as well.  Obviously, I want to
get the problem at hand taken care of, but I'd like to choose a path
that will grow elegantly in the future.


And, thinking of the future, any ideas on how the type system should
bear on collections (like vectors, linked lists, structs)?

;;For example:
(integer-vector 4 5 6)
(float-vector 4.0 5.0 6.0)
;;vs.
(vector \i 4 5 6)  ;;overloading like this s.b. simple
(vector \f 4.0 5.0 6.0)
;;vs.
(vector someType x y z) ;;hmmmm
(apply vector someListWhichMaybeHasTypeInfo) ;;??

Obviously, if flexible coding is wanted, dynamic typing (or at least
type inference) is demanded.  But what route could I go with static
typing that will sacrifice the least coding flexibility?

Thanks,

Chris Perkins

Using \i, \f, etc. for types is terrible (what is \n?). Use names. INTEGER a
nd
FLOAT are much easier to read and understand. Consider also user defined typ
es.

One can have optional type specifiers grafted onto lambda and let expression
s.

Untyped:

(lamda (s v) ...)
(let ((i 2)) ...)

Typed:

(lamda ((s string) (v vector)) ...)
(let ((i integer 2)) ...)

--
Cheers,                                        The Rhythm is around me,
The Rhythm has control.
Ray Blaak                                      The Rhythm is inside me,
rAYblaaK@STRIPCAPStelus.net                    The Rhythm has my soul.

cperkins wrote:
> At the moment, this DSL just needs vectors, basic integers, and
> functions and probably mutliple return values and floats.
> ...
> And, no, no type inference now.
> ...
> So, my question is, what's the best way of adding static typing to a
> subset of the Scheme syntax?

Type inference for what you've described is not difficult.  Why are you so
against the idea?

David

I'm not against the idea, per se.  But having to support type inference
is just one more thing that takes me farther afield of my goal.

Writing a simple compiler isn't too challenging, but every direction
that it might possibly grow in the future presents further design
complications (garbage collection, closures, macros,  threads, etc.).
So, at this early stage I'm trying to minimize my "commitment". My
worry is that type inference might be easy now, but much more complex
later.

I'm definitely not opposed to supporting type inference later - in
fact, I'd love it, and I'll try and plan for it in the very first
design, but it'll have to wait.

Chris

> (let ((x 4 \i) ;;<- the type specifier comes after
>     (y (foo) \v))
>   ...)

Maybe you'd like how they do it in the ML/Haskell world...

(let ((x  4::Int)
(y (foo)::Vec))

Greg Buchholz

cperkins wrote:
> So, my question is, what's the best way of adding static typing to a
> subset of the Scheme syntax?
>
> Common Lisp uses (declare), but that's so wordy, and it puts the type
> declarations a bit away from the variable declarations.   And how to
> handle type inside a (let) statement?

I've also played with the idea.  Something like

(define (some-function int a Airplane b)
(fly b a))

(let ((Airplane a (new-Airplane))
(int n 5))
(some-function a n))

might be not too unreadable.  I don't know if Lisp-style keywords
are read as symbols in Scheme.  Then you could write

(define (bla :int a :Train b) ...

--
No man is good enough to govern another man without that other's
consent. -- Abraham Lincoln

cperkins wrote:
> I'm not against the idea, per se.  But having to support type inference
> is just one more thing that takes me farther afield of my goal.

It wasn't clear to me what your goal was.  Type-directed optimizations?

> Writing a simple compiler isn't too challenging, but every direction
> that it might possibly grow in the future presents further design
> complications (garbage collection, closures, macros,  threads, etc.).
> So, at this early stage I'm trying to minimize my "commitment". My
> worry is that type inference might be easy now, but much more complex
> later.

But why would type inference grow in complexity?  Because your language of
types has changed in some way.  By annotating programs you don't avoid the
problem, in fact you've made it worse-- program annotations must be changed,
not just the compiler.  And I would think any system in which types are not
easily inferred, types will not be easily annotatable either.

By relying on type inference, your programs make no commitment to a specific
type analysis, beyond the commitment that any future type system must have a
decidable inference problem (or not, Scheme programmers don't seem to mind
that their compiler might not halt, since their "lightweight compiler API" i
s
Turing-complete).  Also, for some type systems it's not at all clear how you
could annotate a program with types (for example, a type system for
context-sensitive flow analysis).

David

--
[Hindley-Milner type inference] is clearly the worst thing that
anyone in CS ever came up with.  -- Matthias Felleisen

cperkins wrote:

> Here are the ideas I've had so far:
>
> (defun myFunc (x y)
>   (declare-types \i \i -> \i \i)
>    ;; \i means integer, this function takes two integers and returns
> two integers.
>   ...)
>
>
> or
>
> (let ((x 4 \i) ;;<- the type specifier comes after
>       (y (foo) \v))
>   ...)

It is not clear for me what you are pursuing.

However, in Bigloo I would write:

(define
(myFunc::bint x::bint y::bint z::vector s::bstring k::pair
d::ClassComplex)
(let ((x::bint 2))
..)

Schneewittchen

Ulrich Hobelmann wrote:

> are read as symbols in Scheme.  Then you could write
>
> (define (bla :int a :Train b) ...

What is the problem with Bigloo in that respect?

Schneewittchen

David Van Horn wrote:

> [Hindley-Milner type inference] is clearly the worst thing that
> anyone in CS ever came up with.  -- Matthias Felleisen

Did he really say that?!