Trying to see if I can implement type inference on a toy Lisp, but can't figure out what the type of (car '(x y z)) should be in compile time. For those with experience in dealing with types and Lisp, can I keep these heterogenous lists and Hindley-Milner's algorithm W at the same time - or will they naturally run at odds (which is what I'm thinking)?
I think you need to run dataflow analysis. There is a paper I read which explains the approach, but I lost the link. It describes how to propagate types to optimize code, but the exact same method can be used to type check code too.<p>Basically the compiler annotates each value it deals with with what it knows about it. So in your example:<p><pre><code> (sqrt (car '(1 2 "hello"))
</code></pre>
First '(1 2 "hello") what do we know about it? The value is of type list, the elements types are: integer, integer and string. Since it is a literal, we even know the values: 1, 2, "hello".<p>We record it somehow. Next we apply car to that value. What do we know about the resulting value? If car was a random function, we wouldn't know anything about the result. But car is not random. It is one of the most common Lisp functions so we have custom code for this "known" function that says that its value is the first item of its first parameter.<p>Therefore the type of (car '(1 2 "hello") is integer and the value is 1. Since the type of sqrt is an integer N >= 0 (let's ignore negative roots), the expression (sqrt (car '(1 2 "hello")) type checks! And if we have annotated car and sqrt as side-effect free we can fold the whole expression to 1.<p>Note that if the expression was (sqrt (car '(x y z)) where x, y, z are unknown variables then it would be a "maybe". We can't know if the code type checks or not. Note also that if the expression was (sqrt (car '(-1234 y z)), then the code would <i>not</i> type check as (sqrt -1234) has no type (ignoring complex numbers here). That is strictly more powerful than ordinary type systems which can't determine that (sqrt -1234) is a programming error.
You want a statically typed Lisp dialect?<p>Why don't you just declare your list, say, x, as having type (List Any) where Any is the most general type? (car x) would then have type Any at compile time (i.e you don't know its type), so you can't take its square root or cons it onto a list of type (List Int), but you could still print it or cons it onto another list of type (List Any).<p>(List Any) then has to be distinct from (List ?x) where ?x is an undetermined type. If y is of type (List ?x) and your function contains (sqrt (car y)), you can infer that ?x is a numeric type and y is a list containing only that type of elements.
It depends on the implementation, but even if you have proper type inference, I don't understand how it would help with a heterogenous list, since it's the heterogenous nature that will prevent optimization anyway, even if you knew exactly what the types were.<p>Most lisps, and certainly common lisp, do not depend on type inference for correct behavior in any way, as they are fundamentally strongly but dynamically typed (like Python). The reason for type inference in Lisps is generally for optimization, where knowing that an array is of type X lets you compile X-specific code for functions that take arrays of type X, and to allow efficient memory layout, where your array is made up of contiguous X objects, rather than storing an array of pointers to X objects, and all the cache missing and so on that this causes (as well as overhead of allocating space for the pointers). Just for completeness, I am saying that in the absence of type information, arrays are always actually arrays of pointers.<p>So lists are always made up of cons cells which contain pointers, so one optimization is out regardless (it is possible that primative types like int or float would be packed into the cons cell itself, but most implementations would achieve this by some kind of bit tagging rather than type information being 'known'). The other optimization is out because it would likely be equivalent to do dispatch via the usual method for untyped objects rather than trying to do somehow use the type information.
I'm not exactly sure. I think they may be at odds. Scala can handle AnyTypes in lists, but I think you have to decide whether you want compile time type checking or run time dynamic type checking as from my knowledge you can't have heterogenous lists in languages like OCaml (and from the little I know of Haskell, Haskell as well).
> <i>can't figure out what the type of (car '(x y z))</i><p>What? (quote (x y z)) is a constant expression denoting the value (x y z). We know statically that its car is x, of symbol type.
Perhaps it could infer statically typed tuples from heterogeneous types and then apply list semantics to the operations? If the default is immutability, then all lists can be treated that way heterogeneous or not.<p>SMLNJ and other Hindley-Milner based type inferring languages are good at inferring tuples at compile time so there's probably a little prior art.
could be something like this (with some sugar)?<p><pre><code> data Cons a b = Nil | ConsCell a b
cons = ConsCell
car Nil = error
car (ConsCell a b) = a
cdr Nil = error
cdr (ConsCell a b) = b
mylist = cons 'a' $ cons True $ cons "hello" Nil
mylist :: Cons Char (Cons Bool (Cons [Char] (Cons a b)))</code></pre>
The actual elements of the lists are typeless basically. The easiest way to do this is that each car of a cons cell is just a pointer to a value (actually both are).
Many lisps use tagged pointers where the tag stores the value or even each variable could be a struct with the type and value.