Home > Archive > Scheme > May 2005 > best way to specify static typing?
You are viewing an archived Text-only version of the thread.
To view this thread in it's original format and/or if you want to reply to
this thread please [click here]
| Author |
best way to specify static typing?
|
|
| cperkins 2005-05-01, 9:10 pm |
| 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
| |
| Ray Blaak 2005-05-01, 9:10 pm |
|
Using \i, \f, etc. for types is terrible (what is \n?). Use names. INTEGER and
FLOAT are much easier to read and understand. Consider also user defined types.
One can have optional type specifiers grafted onto lambda and let expressions.
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.
| |
| David Van Horn 2005-05-01, 9:10 pm |
| 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
| |
| cperkins 2005-05-01, 9:10 pm |
| 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
| |
| Greg Buchholz 2005-05-01, 9:10 pm |
| > (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
| |
| Ulrich Hobelmann 2005-05-01, 9:10 pm |
| 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
| |
| David Van Horn 2005-05-01, 9:10 pm |
| 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" is
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
| |
| Förster vom Silberwald 2005-05-01, 9:10 pm |
| 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
| |
| Förster vom Silberwald 2005-05-01, 9:10 pm |
|
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
| |
| alex goldman 2005-05-01, 9:10 pm |
| 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?!
| |
| alex goldman 2005-05-01, 9:10 pm |
| cperkins wrote:
> (defun myFunc (x y)
> (declare-types \i \i -> \i \i)
> ;; \i means integer, this function takes two integers and returns
> two integers.
> ...)
>
It's ugly, because it's not S-expr. How about something like this:
(define (map f lst)
(declare-type
(free (a b)
(-> (-> a b) (list a)))
;; ...
)
| |
| alex goldman 2005-05-01, 9:10 pm |
| (corrected version)
alex goldman wrote:
> cperkins wrote:
>
>
> It's ugly, because it's not S-expr. How about something like this:
>
> (define (map f lst)
> (declare-type
> (free (a b)
> (-> (-> a b) (list a) (list b)))
> ;; ...
> )
| |
| Förster vom Silberwald 2005-05-01, 9:10 pm |
|
alex goldman wrote:
> It's ugly, because it's not S-expr. How about something like this:
>
> (define (map f lst)
> (declare-type
> (free (a b)
> (-> (-> a b) (list a)))
> ;; ...
> )
I am no Lisp expert, but it reminds me somehow on Lisp its type
declaration pitas. I mean such type declarations bear some
un-readability in it - at least in my book.
I love Bigloo its type system and the way one can use it. My background
was Clean prior to using Bigloo. I am not sure whether I would program
in Scheme without having the possibility to give some basic types. In
OCaml for example one could give type tags too. However, OCaml
community is rather weak in teaching such practices.
Surely, there are some weak points relating to Bigloo its type system.
For example it would be rather impossible to create a class which
checks whether your vector consists of integer values only. I haven't
found out a way yet which may check for such a vector type in a
consistent way.
For me: Bigloo its type declarations help me a way lot towards
debugging my code.
Schneewittchen
| |
| Matthias Buelow 2005-05-01, 9:10 pm |
| "Förster vom Silberwald" <chain_lube@hotmail.com> writes:
>I am no Lisp expert, but it reminds me somehow on Lisp its type
>declaration pitas. I mean such type declarations bear some
>un-readability in it - at least in my book.
But type declarations are just a performance hack in Lisp, that are to
be applied sparingly in inner loops (if at all)... I don't think more
verbose (and as ordinary s-expressions) type declarations are a
pita.. they fit in well with the concept of the language. I mean, you
could of course make an S-expression based version of ML or Haskell.
But that isn't Scheme anymore, then.
There seems to be a tendency among some Scheme users to move away from
the clean expressiveness of Scheme and towards a lot more syntax
(either explicit or implicit by naming conventions). I hope this was
just a non-representative observation and isn't going to stick.
mkb.
| |
| Sunnan 2005-05-01, 9:10 pm |
| Förster vom Silberwald wrote:
> For me: Bigloo its type declarations help me a way lot towards
> debugging my code.
I'm not sure I've ever made a type bug. How are they supposed to look,
so I know what to look for? What mistake is there to make?
| |
| Förster vom Silberwald 2005-05-01, 9:10 pm |
| Sunnan wrote:
> F=F6rster vom Silberwald wrote:
>
> I'm not sure I've ever made a type bug. How are they supposed to
look,
> so I know what to look for? What mistake is there to make?
For me it is so much easier to read the following after a long day:
=3D=3D
(define (erg::obj x::bint y::vector z::Complex etc...))
=3D=3D
instead of:
=3D=3D
(define (erg x-val y-vec z-complex etc...)
=3D=3D
One will need a rather strict programming discipline in the latter
case. That sounds easy as long as you only have to deal with small
programs.
The Bigloo compiler is not perfect and it is by no means a static type
analyzer as opposed to Clean for example. However, Bigloo does some
basic type analysis that means if you pass a vector lets say to a
function which expects a class of some tpye you will get a compile
error.
For me types in Bigloo are means for documenting my code.
Schneewittchen
| |
| Sunnan 2005-05-01, 9:10 pm |
| In-Reply-To: <1114879541.512874.26920@o13g2000cwo.googlegroups.com>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 8bit
Lines: 30
Message-ID: <ZDPce.23016$d5.168627@newsb.telia.net>
Date: Sat, 30 Apr 2005 17:55:05 GMT
NNTP-Posting-Host: 213.65.121.239
X-Complaints-To: abuse@telia.com
X-Trace: newsb.telia.net 1114883705 213.65.121.239 (Sat, 30 Apr 2005 19:55:05 CEST)
NNTP-Posting-Date: Sat, 30 Apr 2005 19:55:05 CEST
Xref: number1.nntp.dca.giganews.com comp.lang.scheme:57921
Förster vom Silberwald wrote:
> For me it is so much easier to read the following after a long day:
>
> ==
> (define (erg::obj x::bint y::vector z::Complex etc...))
> ==
>
> instead of:
>
> ==
> (define (erg x-val y-vec z-complex etc...)
> ==
There's also the third alternative, using keyword arguments. This allows
for flexible, documented code that can grow organically - you can update
the function definition without having to change all the call sites.
And I personally don't think that the basic type of variables is very
useful documentation. I'm more concerned with what they represent.
I'd use (erg x y z), possibly augmented with keywords.
I've used Chicken's foreign-lambdas, where you have to specify type, and
I'm always happy when I go back to regular scheme, regular lambdas where
you don't have to do it.
And I still don't understand what these mythical "bugs" that this is
supposed to catch are. I'm sure they exist, otherwise Eiffel and friends
wouldn't be so popular. I just don't know what category of bug this is
catching.
| |
| Marcin 'Qrczak' Kowalczyk 2005-05-01, 9:10 pm |
| Sunnan <sunnan@handgranat.org> writes:
> And I still don't understand what these mythical "bugs" that this is
> supposed to catch are. I'm sure they exist, otherwise Eiffel and
> friends wouldn't be so popular. I just don't know what category of bug
> this is catching.
The most important case is changing some internal API and then
tracking all places where changes need to be propagated to.
--
__("< Marcin Kowalczyk
\__/ qrczak@knm.org.pl
^^ http://qrnik.knm.org.pl/~qrczak/
| |
| Sunnan 2005-05-01, 9:10 pm |
| Marcin 'Qrczak' Kowalczyk wrote:
> The most important case is changing some internal API and then
> tracking all places where changes need to be propagated to.
>
Thanks, that might make sense.
| |
| Sunnan 2005-05-01, 9:10 pm |
| Sunnan wrote:
> Marcin 'Qrczak' Kowalczyk wrote:
>
> Thanks, that might make sense.
Then again - huh?
If I have an internal API function that emits strings and it changes to
emit numbers, of course everything that only works on strings are going
to choke on it - hopefully leaving nice error messages. Everything that
works on everything should still just work, just nicely pass it along.
Why would I need to, or want to, have explicit type information in my
program in order to catch bugs?
....oh. You mean at *compile time*. But that's no replacement for
testing, anyway, is it?
| |
| Marcin 'Qrczak' Kowalczyk 2005-05-01, 9:10 pm |
| Sunnan <sunnan@handgranat.org> writes:
> ...oh. You mean at *compile time*. But that's no replacement for
> testing, anyway, is it?
It's hard to cover every corner by tests. And a type error usually
makes easier to see what needs to be changed than a test failure.
Consider a compiler with several representations of code between
phases. Type definitions of these trees serve as a contract for one
phase to produce and another to consume.
It's not complete, e.g. invariants about scopes are not explicitly
wrttten out in code, but it's better to have a partial specification
than no specification.
When I decide that something needs to be changed, e.g. that values of
floating point literals of compiled code should be represented by sign
+ mantissa + exponent instead of by rational numbers, or that a node
for variable definition should belong to those which include the
source location, or that boolean primitive operations should have a
different kind of node than other primitive operations - it's nice to
change the type definition first, and let be informed about places
where I don't cover all cases, where I unnecessarily cover cases which
are now impossible, or where code must be changed because the data
representation changed. Almost all changes involve changes in types.
* * *
An important helpful error spotted by compilers of statically typed
functional languages is "set of patterns is not exhaustive". Such
error can be generated because the compiler is informed about all
cases a value can have. Using typeless lists with symbols doesn't
give the compiler sufficient information, and isn't easily covered
by tests - enumerating all significant forms of inputs is a lot
of work.
* * *
I don't claim that static typing is in all respects better, or even
that its advantages outweigh the di vantages. I just point out that
significant advantages exist. I miss easy refactoring now that I
mostly switched to dynamic typing.
--
__("< Marcin Kowalczyk
\__/ qrczak@knm.org.pl
^^ http://qrnik.knm.org.pl/~qrczak/
| |
| alex goldman 2005-05-01, 9:10 pm |
| Förster vom Silberwald wrote:
>
> I am no Lisp expert, but it reminds me somehow on Lisp its type
> declaration pitas. I mean such type declarations bear some
> un-readability in it - at least in my book.
>
> I love Bigloo its type system and the way one can use it. My background
> was Clean prior to using Bigloo. I am not sure whether I would program
> in Scheme without having the possibility to give some basic types. In
> OCaml for example one could give type tags too. However, OCaml
> community is rather weak in teaching such practices.
>
> Surely, there are some weak points relating to Bigloo its type system.
> For example it would be rather impossible to create a class which
> checks whether your vector consists of integer values only. I haven't
> found out a way yet which may check for such a vector type in a
> consistent way.
>
> For me: Bigloo its type declarations help me a way lot towards
> debugging my code.
>
> Schneewittchen
Whoah! Is this the first post this year, in which you forgot to mention you
are doing Ph.D. in Physics?
| |
| Ulrich Hobelmann 2005-05-01, 9:10 pm |
| Förster vom Silberwald wrote:
> Ulrich Hobelmann wrote:
>
>
>
>
> What is the problem with Bigloo in that respect?
I don't know. I haven't tried it. So far I only used standard
Scheme. Now I'm learning Lisp, so no Scheme. Maybe I'll retry it
when R6RS is ready.
--
No man is good enough to govern another man without that other's
consent. -- Abraham Lincoln
| |
| Sunnan 2005-05-01, 9:10 pm |
| Marcin 'Qrczak' Kowalczyk wrote:
> Consider a compiler with several representations of code between
> phases. Type definitions of these trees serve as a contract for one
> phase to produce and another to consume.
But maybe it doesn't make sense for all of those layers to have as
strict contracts to each other. For example:
(apply atom-consuming-computation (reverse list-producing-computation)))
If I change the type of the atoms in the list the
list-producing-computation outputs, I shouldn't have to change
"reverse", right?
> I don't claim that static typing is in all respects better, or even
> that its advantages outweigh the divantages. I just point out that
> significant advantages exist.
Which was all I asked - an explanation of what the claims are, rather
than an explanation of why the claims are true/good.
> I miss easy refactoring now that I mostly switched to dynamic typing.
A what now? Aren't many of those refactorings unnecessary in a
dynamically typed language?
(Maybe if I ever understood this issue, I'd turn into someone who likes
Eiffel.)
| |
| Marcin 'Qrczak' Kowalczyk 2005-05-01, 9:11 pm |
| Sunnan <sunnan@handgranat.org> writes:
>
> But maybe it doesn't make sense for all of those layers to have as
> strict contracts to each other. For example:
>
> (apply atom-consuming-computation (reverse list-producing-computation)))
>
> If I change the type of the atoms in the list the
> list-producing-computation outputs, I shouldn't have to change
> "reverse", right?
I don't understand.
>
> A what now? Aren't many of those refactorings unnecessary in a
> dynamically typed language?
No, the need of refactoring has nothing to do with the type system.
Perhaps I shouldn't have used the word "refactoring". I specifically
meant adapting code to synchronize with incompatible changes in code
or data it uses.
In a statically typed language I get alerted when a name that code
refers to is no longer defined, when the number of arguments doesn't
match, or when their types don't match.
In my dynamically typed language I tried to retain as much of this
as possible while having dynamic typing. Undefined global names
are caught, wrong record field names are not caught, the number of
arguments is caught when the function is called directly, types are
not caught. Non-exhaustive matches are not caught at compile time
(but they signal an error at runtime instead of returning a dummy
result).
I don't like when a language catches nothing besides syntax erorrs
at compile time, even undefined names and obvious arity mismatches.
I think in Scheme catching these errors may require whole program
analysis, depending on the module system.
--
__("< Marcin Kowalczyk
\__/ qrczak@knm.org.pl
^^ http://qrnik.knm.org.pl/~qrczak/
| |
| Sunnan 2005-05-01, 9:11 pm |
| Marcin 'Qrczak' Kowalczyk wrote:
>
>
> I don't understand.
I'm showing my ignorance because I don't really understand this issue.
> In a statically typed language I get alerted when a name that code
> refers to is no longer defined, when the number of arguments doesn't
> match,
Aha! I see. Yes, that is a large class of bugs. Now I see what the hype
has been about.
> or when their types don't match.
What does that mean?
In some languages, in order to make a function to swap two variables,
you'd have to declare one function to swap two ints, one to swap two
strings, and so on, right?
That's what you might get when you want all the middle layers to be as
contract-bound as the top and bottom layer.
> I don't like when a language catches nothing besides syntax erorrs at
> compile time, even undefined names and obvious arity mismatches. I
> think in Scheme catching these errors may require whole program
> analysis, depending on the module system.
>
Couldn't you have one type-inferring, error-detecting pass?
| |
| Marcin 'Qrczak' Kowalczyk 2005-05-01, 9:11 pm |
| Sunnan <sunnan@handgranat.org> writes:
>
> What does that mean?
>
> In some languages, in order to make a function to swap two variables,
> you'd have to declare one function to swap two ints, one to swap two
> strings, and so on, right?
These are quite poor type systems (C, old Java, old C#).
In ML, Haskell, Clean, Mercury etc. functions which work uniformly on
all types are as easy to write as functions which work on a concrete type.
OTOH it's harder to write functions which work non-uniformly, i.e. if
they do different things depending on the type.
In addition even if a type is constrained to be concrete, typically
it's written in few places. You don't have to explicitly write types
of function parameters or results.
>
> Couldn't you have one type-inferring, error-detecting pass?
In theory, to some extent - perhaps. I haven't heard of a successful
practical design of this.
An important source of type constraints in statically typed languages
is definitions of structured data types; more important than function
bodies. In a dynamically typed language valid forms of data are not
specified explicitly, they have to be inferred from code which creates
or examines them, which is hard.
It's rare when a compiler can prove that a certain piece of code would
always yield a type error. Perhaps the rest of the program never feeds
it with data which would lead to the error. In the absence of formal
rules about which programs should be considered type correct, the
compiler can't flag a suspicious fragment as erroneous merely because
it can't prove that it's always type-correct. It could only try to be
helpful by warning about places which look suspicious.
--
__("< Marcin Kowalczyk
\__/ qrczak@knm.org.pl
^^ http://qrnik.knm.org.pl/~qrczak/
| |
| Förster vom Silberwald 2005-05-01, 9:11 pm |
| alex goldman wrote:
> Whoah! Is this the first post this year, in which you forgot to
mention you
> are doing Ph.D. in Physics?
Hi:
[A tip: Assuming you are posting via Google. The other day I found out
that replying via Google is made easier if you press the "show
options".]
There is a reason why I always tag my posting -- at least in some
related programming language newsgroups -- with my PhD in physics. I am
not bragging about my PhD (I am a bad scientist; ask the peer-reviewers
of my papers), though.
However, when I was googling around whether Scheme is appropiate for
simulations in physics I didn't really got a motivation for using it.
It was rather this that a lot of comments dragged one into the
believing that Scheme is unsuitable for such tasks.
That is my mission. I mean it is rather redundat to claim in Fortran
newsgroups that you were using Fortran for numerical simulations.
However, Scheme and all the other minor languages deserve some
cheerleading.
Nachrichtensprecher
| |
| Sunnan 2005-05-01, 9:11 pm |
| Marcin 'Qrczak' Kowalczyk wrote:
> These are quite poor type systems (C, old Java, old C#).
>
> In ML, Haskell, Clean, Mercury etc. functions which work uniformly on
> all types are as easy to write as functions which work on a concrete type.
Thanks for this important clarification.
| |
| Per Bothner 2005-05-05, 8:58 pm |
| cperkins wrote:
> So, my question is, what's the best way of adding static typing to a
> subset of the Scheme syntax?
In Kawa you can do things like:
(define (fun (arg1 :: <integer> ) #!optional (arg2 :: <list> '()))
:: <list> ;; optional return-type specifier
... body ...)
(define-class <C1> ....)
(let ((x :: <C1> C1-expression)
(j :: <int> )) ;; Delareres j to be a 32-bit unboxed integer
...)
(define N :: <integer> 100)
(define SB :: <java.lang.StringBuffer> (make <java.lang.StringBuffer> )))
|
|
|
|
|