 A Type Notation for Scheme
started 9/25/2002; 2:40:00 AM - last post 10/3/2002; 3:58:40 AM
|
|
jon fernquest - A Type Notation for Scheme 
9/25/2002; 2:40:00 AM (reads: 2002, responses: 5)
|
|
| A Type Notation for Scheme |
|
A lightweight type notation and type checker for Scheme.
The type annotations can be added to already existing code
in a file separate from the Scheme
source code.
These types "can also be thought of as abstractions of the type predicates
found in Scheme."
There is a nice table giving the "correspondence between types, predicates, and expressions"
is also given.
There is also a
PDF version
PDF Version
of the paper.
The paper
Polymorphic Type-Checking in Scheme
(Jenkins-Leavens, 1996) provides a broader overview of the notation.
Posted to implementation by jon fernquest on 9/25/02; 2:49:18 AM
|
|
|
|
jon fernquest - Re: A Type Notation for Scheme
9/25/2002; 3:09:13 AM (reads: 867, responses: 0)
|
|
|
The Jenkins-Leavens type annotation
might be useful in a more *incremental, evolutionary approach to software development*
in which typing is added as a program grows larger and more
complex (allowing you to break abstractions easily when the program
is small while making sure the program maintains its integrity and doesn't
collapse as it grows larger
as Cardelli suggests in his "Typeful Programming" paper and as was discussed in a
very long thread).
There are other Scheme type systems.
Andrew Wright's PLT Scheme soft type checking seems
goes hand in hand with input argument pattern matching.
Bigloo Scheme also has "explicit typing"
http://www-sop.inria.fr/mimosa/fp/Bigloo/doc/bigloo-15.html
Has anyone compared these different systems?
The source for this system is a course resources page:
http://www.cs.iastate.edu/~leavens/ComS342-EOPL2e/resources.shtml
The source code file 'type-check-and-eval.scm'
needed to run the type checker is in the directory:
http://www.cs.iastate.edu/~leavens/ui54/lib/
|
|
Ehud Lamm - Re: A Type Notation for Scheme
9/27/2002; 5:21:08 AM (reads: 748, responses: 0)
|
|
|
I finally had the time to follow this link. It is very well written, and explains many important concepts.
|
|
Alex Moffat - Re: A Type Notation for Scheme
9/28/2002; 6:57:56 PM (reads: 699, responses: 0)
|
|
|
|
Noel Welsh - Re: A Type Notation for Scheme
9/30/2002; 2:25:13 PM (reads: 705, responses: 0)
|
|
|
Has anyone compared these different systems?
Bigloo's type system revolves around enabling compiler optimisations and only supports simple "C-like" types. So no polymorphism or even function types!
Soft typing infers types and has a type system similar in expressivity to MLs. Soft typing never rejects a program; it just insert checks where it can't prove a program safe. The refinements of soft typing (MrSpidey and now MrFlow) are getting quite funky, with user interfaces that show how values flow around the program (good for understanding why a check is needed) and quite expressive type systems.
|
|
jon fernquest - Re: A Type Notation for Scheme
10/3/2002; 3:58:40 AM (reads: 693, responses: 0)
|
|
> Soft typing infers types and has a type system similar in
> expressivity to MLs...
Do you know of anyone who has got soft typing and units to work with implmentations other than MzScheme. I think MzScheme is great, I'm just wondering how portable soft typing is?
|
|
|
|