Lambda the Ultimate

It reminded me (based on reading the paper) more of the type of things done in C# than type inference in the HM world.

This is definitely the idea. There's currently two main places where types are inferred: local variable bindings, and polymorphic function applications. This is definitely the majority of the annotation 'burden', in my opinion. Annotations on top level definitions are useful to have, independent of type system.

There are plans for somewhat more inference, along the lines of Pierce and Turner's Local Type Inference, but that has not yet been implemented.

Thanks for the interest in the paper, by the way. If people want to try out Typed Scheme, they can find it here.

As James Iry's noted, one can implement Scheme in Haskell, and this suggests a rather obvious way of implementing types in a Scheme variant:
Compiling a 'Typed' scheme to Haskell with error messages etc. suitably translated to make sense in the 'typed scheme' language.

Obviously this would have Haskell-type types rather than the ones in the paper discussed here..

Has anyone tried this? I'm sure there are plenty of issues with making this a 'practical' implementation, but it seems like it would be a very interesting experiment.

At least it might be useful for parsing scheme, looking for latent type errors and unboxing optimizations.

Perhaps this could tie in with the (rather different) work on making scheme-like version of the ACL2 language for proving theorems about code.

A Lispy Haskell has been discussed here before. It's definitely not Scheme, though.

Thanks for pointing that out.. There is a website now, liskell.org.

Although the website makes the project look rather inactive, it does mention "A top-level-less Scheme compiler" as one of its "technology demos" (here).
The implementation looks rather short, though.

At least it might be useful for parsing scheme, looking for latent type errors and unboxing optimizations.

Not really. Without its own type analysis, all that such a translation can handle is the subset of Scheme programs that can have their types fully statically inferred when translated to Haskell. Any resulting errors are errors with respect to the Haskell type system and its limitations when it comes to dealing with unitypes. Most such errors wouldn't be actual errors in the original Scheme program.

That's not to say that such a translation might not be useful for other purposes, but it's not useful for checking types in ordinary Scheme code.

Fritz Henglein, in the 90's, wrote a system for converting Scheme programs to ML programs and minimizing the resulting tag checks. You can find the papers here:

http://library.readscheme.org/servlets/search.ss?pattern=Henglein+Fritz

The difference between what you suggest and Typed Scheme is, of course, that different programs typecheck. For example, there's no subtyping in Haskell, so you'd have to add lots of injections and projections (that's what Henglein wrote about). Also, this program in Scheme:

(map add1 (filter number? l))

where l is some list of arbitrary elements, is not going to typecheck in Haskell, whereas it does in Typed Scheme.

(map add1 (filter number? l))

That's the coolest part of this work, ain't it?

And seems to be related to Gradual Typing with Unification-based Inference.

"Gradual typing with unification-based inference" is a purely theoretical investigation of type inference in a world of partial type annotations. It is my impression that the paper assumes a type algebra similar to that of ML or Haskell -- i.e., an algebra over arrows and the usual constructors -- and that kind of type theory can't deal with the example that Sam put up. [Please prove me wrong if this is incorrect.]

To assign types to this kind of expression (without casts) you need something like dependent types or our notion of _occurrence typing_. It is an explicitly static discipline that relies on annotations at the moment. Having said that, our small experience with a few thousand lines of "real" programming suggests that this notion is not only theoretically sound but highly practical.

Research on inference welcome. User reports on Typed Scheme even more welcome.

...I should have been more careful: I only meant "related to" in the very loose sense that both approaches attempt to resolve the tension between type inference and fully-explicit type declarations in an unobtrusive fashion. No doubt there are important theoretical and pragmatic differences between them that I will have to learn a great deal more about. :-)

I intend to check out Typed Scheme (if you haven't read Anton's comments here, you should; he makes PLT Scheme seem very attractive).

What is your opinion on the Typed Scheme type system vs a type system similar to that of ML or Haskell? Is the lack of parametricity solvable?

You can program in Typed Scheme as if it were ML, and then use other features when you want to. The major drawback compared to ML in that situation is that the type inference isn't as complete (and can't be). I don't typically find this to be a significant issue - I would prefer if more ML programs made somewhat less use of type inference. As for Haskell, the type systems are quite different - I'm not sure comparing them is terribly useful.

As for parametricity, I'm not sure whether you're asking about polymorphism in general, which Typed Scheme has, or the fact that polymorphic functions in Typed Scheme can behave differently for different argument types. I don't think this is a problem - the only loss I know of is Wadler's free theorems, which I don't ever think about anyway.

Thanks for your interest in Typed Scheme.

polymorphic functions in Typed Scheme can behave differently for different argument types

Interesting that you should phrase it like that. Indeed, the limitation of H-M types that you seem to be implying here seems to be one of those things that was, and has been, for a long time believed to be true (at least in the practical sense). Nevertheless, it is a false belief. It is perfectly possible to write functions in a H-M typed language whose types (and behavior) depend on the types of their arguments. Just a couple of days ago I wrote a page about one (more) technique, dubbed static sums, that allows such functions to be written.

Edit: clarified

I can't help but feel that if you really intend "H-M typed" to prohibit extensions to H-M then making essential use of the module system is seriously cheating. Or have I missed something?

That said, this also suggests that we rarely care about what can be done with H-M alone.

If you mean the stuff on the static sum page, then I assure you that any use of the module system there is not essential to the technique:

Standard ML of New Jersey v110.67 [built: Fri Jan 11 21:41:45 2008]
- fun inL x (f, _) = f x ;
val inL = fn : 'a -> ('a -> 'b) * 'c -> 'b
- fun inR x (_, g) = g x ;
val inR = fn : 'a -> 'b * ('a -> 'c) -> 'c
- fun match x = x ;
val match = fn : 'a -> 'a
- fun succ s = match s (fn i => i+1, fn r => r+1.0) ;
val succ = fn : ((int -> int) * (real -> real) -> 'a) -> 'a
- succ (inL 1) ;
val it = 2 : int
- succ (inR 2.0) ;
val it = 3.0 : real

I don't see how this is dependent on the types rather than which of inL or inR is used - it's just an encoding of what Haskellers know as Either Int Real, no?

I don't see how this is dependent on the types rather than which of inL or inR is used - it's just an encoding of what Haskellers know as Either Int Real, no?

No it isn't. Please carefully read the page I referred to. If you do that, you should hopefully understand the difference. The technique works at least as well in Haskell.

In case you missed it on the first reading, note that the ordinary/generic sum type described (first to motivate the discussion) on the page is isomorphic to Haskell's Either type. Also note that inL x and inR x, regardless of (the type of) x do not necessarily have the same type (usually they have different types).

Added: I should also point out that, of course, inL x and inR x also evaluate to different values. Two expressions that have different (principal) types generally produce different values (although it is possible to give multiple different types to some expressions).

Added: Here is a ghci interaction that demonstrates the difference between ordinary sum types and the static sum:

Prelude> let succ x = case x of {Left i -> i + 1 :: Int ; Right r -> r + 1.0 :: Double}

<interactive>:1:60:
    Couldn't match expected type `Int' against inferred type `Double'
    In the expression: r + 1.0 :: Double
    In a case alternative: Right r -> r + 1.0 :: Double
    In the expression:
        case x of
          Left i -> i + 1 :: Int
          Right r -> r + 1.0 :: Double
Prelude> let inL x (f, g) = f x
Prelude> let inR x (f, g) = g x
Prelude> let match x = x
Prelude> let succ x = match x (\x -> x + 1 :: Int, \x -> x + 1.0 :: Double)
Prelude> succ (inL 1)
2
Prelude> succ (inR 1)
2.0

BTW, you could (and should) assign more general types to inL, inR, and match in Haskell.

Okay, re-reading it appears to be the standard encoding but with all types left to the typechecker - the same terms you'd use to encode sums in the untyped lambda calculus, with their principal types. This nets you a spare type variable which you can attempt to set a 'return type' with, allowing you to additionally type all cases where you already know which branch you're taking (and deduce which they are via type inference, which is perhaps slightly more useful). Cute, but still doesn't actually let you do anything new with the type info - it just avoids overconstraining in a few scenarios.

Okay, re-reading it appears to be the standard encoding but with all types left to the typechecker - the same terms you'd use to encode sums in the untyped lambda calculus, with their principal types.

Pedantically speaking, that isn't precisely true. The signature given there restrict the types. IOW, the types aren't just left to type inference. One of the restrictions is to ensure that the second argument to match needs to be a pair of functions (and, not, for example, a pair of a function and a list).

Cute, but still doesn't actually let you do anything new with the type info - it just avoids overconstraining in a few scenarios.

Well, the act of discovering a programming idiom obviously doesn't change a type system. You could have written the same functions back in the seventies and have them type checked. So, it isn't, and could never be, "new" in the sense that it would change set of terms that can be typed in a language.

Let me make it clear why the technique is not an encoding of the Either type. The reason is that the Either type can only encode a strict subset of static sum types. For every Either type, there is a corresponding static sum type, but not vice versa. Either types correspond to static sum types that unify with ('dL, 'c, 'dR, 'c, 'c) StaticSum.t. But, as can be seen from the succ example, there are static sum types that do not unify with such a type. So, actually, given a term, new, written in terms of inL, inR, and match, it is not necessarily the case that replacing them with Left, Right, and case, respectively, you would still be left with a term, old, that can be typed.

Just to clarify further, the trick is that (except when unified to be the same) the type of a static sum indicates which variant it is. IOW, like I said earlier, the type of static sum is generally different depending on whether it was constructed with inL or inR. This allows you to write functions, in a H-M type system, whose results depend on the types of their arguments, which was my point. And, of course, those functions are polymorphic. Look at the type of succ. So, spelling it out in full: polymorphic functions in H-M typed languages can behave differently for different argument types.

As Philippa says, this is the standard Church encoding as far as values are concerned but with first order types. Usually typed Church encodings require rank-2 types and there is a reason for that.

The type of the constructors of the Either data type are:
Left :: a -> Either a b
Right :: b -> Either a b

The usual typed Church encoding of the Either data type is:
left :: a -> (a -> r) -> (b -> r) -> r
left x l r = l x

right :: b -> (a -> r) -> (b -> r) -> r
right x l r = r x

This is not a polymorphic as these could be, however, let's say we want to make a list of Either Int Double, e.g.
[Left 3, Right 4.5] :: [Either Int Double]

We can't quite do them with the above, and we can't do them at all with Vesa's inL and inR without losing their "benefit". If Left :: a -> Either a b and left :: a -> (a -> r) -> (b -> r) -> r, Either a b must correspond to
type Either a b = forall r.(a -> r) -> (b -> r) -> r
with this, [Either Int Double] corresponds to the rank-2 type [forall r.(Int -> r) -> (Double -> r) -> r]. So, to use the "static sums" as first-class sums, you need to lose their "benefit". Uses are presumably in approaches similar to Danvy's approach to functional unparsing.

So, spelling it out in full: polymorphic functions in H-M typed languages can behave differently for different argument types.

No, there is no "behaviour depending on the type" (there's certainly types "depending on" types, but that's trivial). The choice is driven (just like for the normal Either data type) by the value constructors, in this case, inL and inR. As far as I can see, to actually get different behaviour based on type you need to support some kind of ad-hoc polymorphism such as Haskell type classes, intensional type analysis or C++ style overloading. The values depend on types (that's parametric polymorphism) but only in a trivial way; namely that we treat the type as a black box, we don't dispatch on it.

Vesa's inL and inR

To set the credits straight, the formulation of the idiom as a kind sum was due to Stephen Weeks (more than a year ago). What I've written here and on the static sum page is based on my own interpretations, of course.

Uses are presumably in approaches similar to Danvy's approach to functional unparsing.

Yes. It was discovered while working on the Fold technique.

No, there is no "behaviour depending on the type"

Forget for a moment that you know how static sums are implemented internally. Treat it as an abstract type with two constructor functions, inL and inR, and one one deconstructor, match, whose types are given by the following signature:

signature STATIC_SUM = sig
   type ('a, 'b, 'c, 'd, 'e) t
   val inL : 'a -> ('a, 'd, 'b, 'c, 'd) t
   val inR : 'c -> ('a, 'b, 'c, 'd, 'd) t
   val match : ('a, 'b, 'c, 'd, 'e) t -> ('a -> 'b) * ('c -> 'd) -> 'e
end

Consider the following example:

- type u = unit ;
type u = unit
- type p = unit * unit ;
type p = unit * unit
- fun adHocery s = StaticSum.match s (fn () => ((), ()), fn ((), ()) => ()) ;
val adHocery = fn : (u,p,p,u,'a) StaticSum.t -> 'a
- val u = StaticSum.inL () : (u,p,p,u,p) StaticSum.t ;
val u = fn : (u,p,p,u,p) StaticSum.t
- val p = StaticSum.inR ((),()) : (u,p,p,u,u) StaticSum.t ;
val p = fn : (u,p,p,u,u) StaticSum.t
- adHocery u ;
val it = ((),()) : p
- adHocery p ;
val it = () : u

As you can see, the types of u and p are different and the adHocery function behaves differently depending on which one it is given. Also, u and p are the only observably different values accepted by the adHocery function. It is impossible to construct any other observably different values accepted by the adHocery function. Essentially, it has been arranged so that there is a one-to-one correspondence between the type of an argument accepted by the adHocery function and the behavior of the adHocery function. So, tracing the dependencies, we get that the value returned by (or the behavior of) the adHocery function depends on the value of the argument, which depends on the type of the argument. Hence, transitively, the behavior of the adHocery function depends on the type of its argument.

Well, of course, this is a logical illusion of sorts. Specifically, the fact that there is a one-to-one correspondence between the type and the value of an argument accepted by the adHocery function, doesn't mean that the dynamic semantics would actually be selected based on the type. However, when reasoning about the adHocery function, it doesn't matter. There just isn't any way to observe anything that would contradict the view that the behavior of the adHocery function depends on the type of its argument or even that the behavior would be selected based on the type.

As far as I can see, to actually get different behaviour based on type you need to support some kind of ad-hoc polymorphism such as Haskell type classes, intensional type analysis or C++ style overloading.

Well, then you'll just need to learn to see farther. Continuing the previous argument, let's play out another thought experiment. Suppose that we have an ML-style language (with first-class polymorphism to make this practical) that has been defined so that integers (literals) have the type

forall ('a, 'b, 'c).(int, 'a, 'b, 'c, 'a) StaticSum.t

and reals have the type

forall ('a, 'b, 'c).('a, 'b, real, 'c, 'c) StaticSum.t

Now, the function plus

fun plus (a, b) =
    (match b o match a)
       (fn a => (fn b => inL (Int.+  (a, b)),
                 fn b => inR (Real.+ (real a, b))),
        fn a => (fn b => inR (Real.+ (a, real b)),
                 fn b => inR (Real.+ (a, b))))

computes the sum of two numbers, integers or reals. Furthermore, it returs a real if at least one of the arguments is a real. Otherwise it returns an integer.

Sidenote: As written above, the plus function compiles even in SML'97 (without first-class polymorphism), but to make the implied usage (all arithmetic based on similarly defined functions) practical, first-class polymorphism is a must. Also, the idea is that the types int and real and the modules Int and Real refer to primitives that wouldn't actually (need to) be exposed to a user of the language.

Now, again, it has been arranged so that the behavior of the plus function is different depending on the types of its arguments. There is just no way to observe anything that would contradict with that view. So, reasoning about the behavior of plus, one can treat it as if the behavior would depend on the types of its arguments.

This is the kind of reasoning that is done in mathematics all the time. You first show that there is a suitable morphism between two kinds of things As and Bs. Then you can treat As as if they were Bs. In this particular case, we have functions whose behavior depends on the values of their arguments. But the sets of argument values that invoke the different behavior also have disjoint sets of types. So, one can treat the functions as if their behavior would depend on the types of their arguments. What part of this kind of reasoning do you disagree with?

What this means is that static sums allow you to encode type dependent functions. The encoding can be faithful in the sense that the encoded terms using static sums type check precisely when the corresponding terms written in the type dependent language, whose terms are being encoded, would type check. Furthermore, that can be done even in a basic H-M type system. To prove this, one needs to device a simple language with type dependent functions, specify an encoding of the terms of that language using static sums, and then prove the usual correspondences between the original type dependent terms and their encodings. Of course, like with many encodings, a whole-program (or whole-term) transformation is needed in the general case. And, of course, in a more expressive type system than H-M, it may be possible to encode more type dependent functions (terms of a more expressive type dependent language) than in the H-M system.

The plus function reminds me very much of GADT-based type classes, under the "case coalescing" section. Is this static sum a limited form of ML GADT?

Forget for a moment that you know how static sums are implemented internally.

I never mentioned how they were implemented internally. How they are implemented is completely irrelevant.

As you can see, the types of u and p are different and the adHocery function behaves differently depending on which one it is given.

They are also different values. Different values tend to behave differently.

Well, of course, this is a logical illusion of sorts. Specifically, the fact that there is a one-to-one correspondence between the type and the value of an argument accepted by the adHocery function, doesn't mean that the dynamic semantics would actually be selected based on the type.

Indeed.

However, when reasoning about the adHocery function, it doesn't matter.

And if the types happen to be the same, it's clear that the types cannot possibly be the discriminator of the behaviour.

Other than that, the types in the static sums restrict the possible values, but that's just what types do anywhere.

On a different note: what is a "type dependent language"? It sounds vaguely like you want a dependently typed language, but that's types depending on values.

And if the types happen to be the same, it's clear that the types cannot possibly be the discriminator of the behaviour.

Yes, of course, but that is not the point. The functions are type dependent --- not the arguments. The behavior of the kind of functions that I'm talking about here is different depending on the types of its arguments. Conversely, a function whose behavior does not correspond to (or depend on) the types of its arguments is not type dependent. And, yes, of course, you can write functions whose arguments are static sums, but whose behavior does not depend on the types of the arguments.

It sounds vaguely like you want a dependently typed language, but that's types depending on values.

From a practical point of view, I think that the technique is suitable for encoding some functions that one might want to write in a dependently typed programming language. Instead of having types depend on values, one changes the types of (argument) values (via tagging them with static sums in this case) and then writes type dependent functions. Compared to some other techniques, static sums may perhaps be more straightforward (idiomatic) to use for some such encodings. With static sums it is almost as if you could do a switch case on types (typecase).

In the story Tagless Staged Interpreters for Simpler Typed Languages, that is one of the techniques that was key to our work. Instead of directly using rank-2 types, we used the module system of ML and the class system of Haskell for the same purpose, as that's all that was needed. And that is also how we get around the problem of parametricity: we don't make the r type abstract, we merely delay its details. There is a huge difference!

It does seem that using the Church encoding (which is really a final algebra encoding) instead of the usual initial algebra semantics does buy you something non-trivial.

I consider losing parametricity (which is what the loss of the free theorems is equivalent to, though admittedly there are degrees of it) a bad thing. However, as I have not read the paper yet, I'm not in a position to comment on how bad the problem would be in Typed Scheme.

Practical Type Inference Based on Success Typings is a paper about inferring type signatures for Erlang functions. The type signatures are different from ordinary types in the sense that the type signature a -> b implies that if the function is called with the type a it might crash or return b, if it is called by something else it will definitely crash. This means that the signature any -> any is a correct signature for all unary functions, so the type inference problem is to infer as exact types as possible

This approach can be used together with the approach of typed scheme to infer some type information for modules which can not be type checked since they rely on invariants which can not be expressed in the type system.

In the gradual type system, we could have the following type assignment:

l : ? list
number? : ? -> bool
filter : ('a -> bool) -> 'a list -> 'a list
add1 : int -> int
map : ('a -> 'b) -> 'a list -> 'b list

Our paper didn't describes 'list' types, but there are two obvious choices: 1) allow variance and do run-time checking on list element access, or 2) don't allow variance. In our Scheme Workshop paper we described references (i.e., one element lists) and went with invariance. It looks like with inference, invariance is still a better choice. Let's consider the example:

(map add1 (filter number? l))

With choice 1) filter is instantiates to (int -> bool) -> int list -> int list and map instantiates to (int -> int) -> int list -> int list and a cast is inserted to coerce the ? list into the int list expected by filter. But this is bad because a cast error occurs on the first non-integer in the heterogeneous list.

With choice 2) filter instantiates to (? -> bool) -> ? list -> ? list and map instantiates to (? -> int) -> ? list -> int list. A cast is inserted to coerce the add1 function from int -> int to ? -> int. So this choice works.

That being said, occurrence typing is a good idea and I look forward to investigating how it can be combined with gradual typing. With occurrence typing I assume you'd get a more accurate type for the result of filter, an int list instead of ? list.

As for the paper being "purely theoretical", it certainly contains a fair amount of theory. This is necessary to make sure that the ideas are correct. However, it is not "purely theoretical" because our intension is for this to be a step towards a type system for a mainstream language. I don't know how long it will take to get there, but I've just hired some great graduate students to work on this.

Several points on this issue:

1. Maybe I'm confused, but it sounds like you said first that
invariance is the better choice, but also that it leads to a runtime
error in this example. Is that right?

2. Is the need for invariance or runtime checks inherent in the
gradual typing system? Typed Scheme has covariant lists, without any
extra checks, and I think they're essential for typing real Scheme
programs.

3. The interesting nature of the example I posted is that Typed Scheme
typechecks the example as-is; that is, without adding additional
runtime checks. If we extend the domain of add1 to include arbitrary
values, then the ML type system can check the example. What your type
system is doing is automatically writing the needed wrapper for the ML
type system to work here. Typed Scheme is doing something very
different - the type of the input list to filter is different from the
return type, and therefore no new runtime checks are needed.

Here's the type of filter in Typed Scheme:

(A -> Bool : B) (Listof A) -> (Listof B)

That is, it takes a function from A -> Bool that checks for type B,
and it produces a list of type B. Note that A and B don't have to be
the same. This is what gives Typed Scheme the power demonstrated in
this example.

4. As for theory vs practice, we've also done theoretical work on
Typed Scheme, but we've also already done lots of practical
investigation, whereas it doesn't sound like that work has been done
yet for gradual typing. I'm glad you plan to do that in the future.

1. Invariance does not lead to run-time errors.

2. If Typed Scheme has covariant lists, then either it doesn't allow set-car! (the list is immutable), or it does runtime checking, or it is unsound. I was assuming mutable lists in the above. For immutable lists, covariance could likewise be allowed in the gradual system without checks. This is standard type theory.

3. Yes, that repeats my point about the return type of filter. Thanks for the further details.

4. When the interlanguage paper was published but before the implementation of Typed Scheme was finished, I didn't say that line work was "purely theoretical". A similar courtesy would be appreciated.