Home

Sage: A Programming Language With Hybrid Type-Checking

Since we've been discussing hybrid type checking, dependent types, etc. recently...

Sage

Sage is a prototype functional programming language designed to provide high-coverage checking of expressive program specifications (types). Sage allows a programmer to specify not only simple types such as "Integers" and "Strings" but also arbitrary refinements from simple ranges such as "Positive Integers" to data structures with complex invariants such as "Balanced binary search trees." In addition to featuring these predicates upon types, Sage merges the syntactic categories of types and terms, in the spirit of Pure Type Systems, to express dependent types such as that of the infamous printf function.

Sage performs hybrid type checking of these specifications, proving or refuting as much as possible statically, and inserting runtime checks otherwise. For the complete details of the theory and empirical results, we direct you to the technical report.

By Paul Snively at 2006-06-04 23:52 | Functional | Implementation | Meta-Programming | Type Theory | other blogs | 14931 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Great paper

Wow, what an amazingly well-written paper! Everyone should read this.

Edit: the use of an automated theorem prover for checking the subtyping relation for refined types results in pretty substantial compile times. Since they already have a refutation/counterexample database with information collected at run-time fed back into the compile-time type checker, I'm surprised they don't have a confirmation/proof database (mapping theorems to booleans or perhaps proof certificates) which is both updated and used by the static type-checker. This enables fast turn-around: each change to the program should result in only a small handful of genuinely new theorems requiring proof, the bulk of the proof burdens being the same as for the previous compilation of the program. Something like this seems essential if you want to scale beyond toy programs.

By Per Vognsen at Mon, 2006-06-05 06:34 | login or register to post comments

Qi

So sorta like Qi only with more compile time checking?

By djb at Mon, 2006-06-05 09:44 | login or register to post comments

Good Question!

djb: So sorta like Qi only with more compile time checking?

"More compile-time checking" is an interesting question relative to Qi, since both Sage and Qi appear to have Turing-equivalent type systems. Both make static typing optional. So I guess one question would be how many lines Qi takes to implement; one thing that I like about Sage is that it's about 5,000 lines of O'Caml—I feel like I could actually get my head around an implementation that small!

By Paul Snively at Mon, 2006-06-05 18:08 | login or register to post comments

On Qi's Size

Qi is programmed in Qi and clocks in at about 4300 lines of code, comments and whitespace included.

Of course, Qi is built atop the monster of Lisp, so I'm not sure it counts. *grin* But if you like wrapping your head around language internals, the source code and comments for Qi do a great job of explaining the internals. So you should check it out. *smile*

By entropyfails at Thu, 2006-11-02 17:22 | login or register to post comments

From What I Read

From a few minute read of the paper, it seems like one of the significant differences is the run time analysis of counter-examples for the type checker and the automation of the hybrid type. In Qi, you have to manually insert "verified" rules to do typesafe transformations. In Sage, they compute an inferred relationship between types. For example, if you have the variable username that was input from the console as a type String and you need to put that into a function auth that takes the type LoginName, the compiler would automatically infer that you want to do forced type transformation, and run the appropriate rules for construction of a LoginName type from a String type. However, if you get a bad string like "admin --#$@", then this obviously not match and an error will be raised during the runtime.

Also, it will add a rule to the counter-example database that basically says, "I have found a String type that is not a LoginName. Do not infer this anymore." While this can optimize the compiler a bit, your counterexample database would have to be discarded any time you changed either of the basic types, so I'm not sold on the value of this yet. *grin*

All in all, it looks like a nice language. I very much like fully computable types.

By entropyfails at Thu, 2006-11-02 17:52 | login or register to post comments