Home » forums » LtU Forum

Static Types vs. Partially Evaluated Latent Types

Here's a question I've promoted from another thread (sorry for the multiple postings).

What's the difference between static type inference (like in Haskell) and a latent (tagged) type system (think Scheme) with a real good partial evaluator? In the type-inference situation, we're using unification to solve a set of constraints. If there's no solution, we give up and say the program was ill-typed. On the other hand, it seems like tag checking code in a latently typed lanugage would be a good candidate to get partially evaluated away at compile time. For example it seems like... 

;; typed values are really pairs of values and types
;; e.g. (123 . 'number)
;;      ("abc" . 'string)
(define (isnumber n) (eq? (cdr n) 'number))
(define (add arg1 arg2)
    (if (and (isnumber arg1) (isnumber arg2))
        (machine-add (car arg1) (car arg2))
        (error "not a number")))

(add '(4 . number) '(5 . number))
...should be easily changed into... 
(machind-add 4 5)
... And after we're done partially evaluating our source, if we still have left over type-check predicates like 'isnumber' in the code then we again declare that the program is ill-typed. Are the two methods comparable in any way? Is one method more powerful than the other, or are they somehow duals of each other? Are there any papers available discussing this?

Anton van Straaten recommends looking at a previous typing thread, and the paper Types as Abstract Interpretations, as well as a posting of his to the LL mailing list. Any futher thoughts?

By Greg Buchholz at 2005-06-23 20:41 | LtU Forum | previous forum topic | next forum topic | other blogs | 7516 reads

Comment viewing options

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

Compile time guarantees

What's the difference between static type inference (like in Haskell) and a latent (tagged) type system (think Scheme) with a real good partial evaluator?

Ignoring decidability, normally, the difference isn't speed but compile-time guarantees. Latent typing, as I understand the definition, would allow
add 4 "hello" as a valid program.


Unfortunately, the informal way you defined latent typing (reject programs where typechecks still occur) is actually, uhm, (a) problematic (how to treat data-types/decidability?) and (b) seems like a form of static typing to me.


[In the end, I guess this is a questionable question. You can compare type systems and type inferencing algorithms but not latent vs static typing. The definitions of the latter being too hazy.]

By marco at Fri, 2005-06-24 07:57 | login or register to post comments

Clairification

...the difference isn't speed but compile-time guarantees. Latent typing, as I understand the definition, would allow add 4 "hello" as a valid program.

I probably wasn't being clear enough in my explaination. Scheme normally allows add 4 "hello", but a sufficiently advanced partial-evaluator should be able to execute the type checking predicates in add at compile time, and flag the error then.

Unfortunately, the informal way you defined latent typing (reject programs where typechecks still occur)

I wasn't trying to define latent typing in that manner, I was merely trying to the term in the sense that Schemers use it.

(b) seems like a form of static typing to me.

Yes, that's the point I was trying to make. I'll try to state it differently. Usually, latent typing only catches errors at run-time, but the type checks that happen at run-time seem like they could be evaluated at compile time if we tried hard enough.

By Greg Buchholz at Fri, 2005-06-24 15:04 | login or register to post comments

Sometimes #doesNotUnderstand isn't an error

In many dynamically typed languages, operations that might be considered "type errors"--such as message sends that return #doesNotUnderstand--are not considered errors by the programmer. It's a common idiom in Smalltalk to test for #doesNotUnderstand and do "something else" when it occurs, such as delegating the message to some other object (which then might be able to handle it instead).

There are many other instances in programming where errors at one level (a subsystem cannot fulfill it's promises so it signals an error via whatever mechanism the language provides) is considered normal behavior by a higher level (the error is expected and handled; and does not represent a failure of the program as a whole).

In some (many?) cases, the conditions in question are beyond the type system--for example, testing for the existence of a configuration file and loading a default if it is absent. Others, though might be amenable to typechecking--a suitable advanced typechecker might prove that a given message send always returns #doesNotUnderstand.

It would be unfortunate for a compiler to reject such a program as invalid, if a #doesNotUnderstand response is considered acceptable in the context where the failing message send occurs.

By Scott Johnson at Fri, 2005-06-24 16:10 | login or register to post comments

I don't know of any direct co

I don't know of any direct comparison such as you mention. In the grandfather of the thread Anton linked to, I posted a similar idea. Paul Snively then hinted at a connection to partial evaluation.

By Kevin Millikin at Fri, 2005-06-24 09:57 | login or register to post comments

Excellent

Your post is a more fleshed-out example of almost exactly what I was thinking. Types represent an approximation to the behavior of our program, so why not have that notation available as program we could run and debug? In fact, maybe we could write and execute the "types program" first, and later come back and fill in the code (or have a "code inferencing" algorithm help us with that). And maybe that's somewhat similar to what Epigram does (I've been too intimidated by all the high-level mathematics behind dependent typing to actually try it out). I've definitely got a lot more to chew on. Thanks.

By Greg Buchholz at Fri, 2005-06-24 14:47 | login or register to post comments

Expressivity of static types

One difference is in Haskell types can be derived from the context of an expression, not merely from values it operates on. For example the monadic return has a different meaning depending on the monad it is used with, and its usage may even be polymorphic.

Given that, I still prefer dynamic typing in general.

By Qrczak at Fri, 2005-06-24 13:17 | login or register to post comments