Ask HN: Can I have heterogenous lists in a Lisp while preserving type inference? | Hacker News Reader

Ask HN: Can I have heterogenous lists in a Lisp while preserving type inference?

21 pointsurs210232 comments

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)?

View on HN

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.

Basically the compiler annotates each value it deals with with what it knows about it. So in your example:

    (sqrt (car '(1 2 "hello"))

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".

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.

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.

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 not 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.

I just saw this - but funnily enough, this is how I handled it. Thanks man - appreciate the comment!

You want a statically typed Lisp dialect?

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).

(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.

So let's try an experiment:

(sqrt (car '(1 2 "hello"))

How would this work according to you, if the car function will return type Any? And what is the difference between ?x and Any?

Thanks by the way!

If that's typed into the listener, it should probably just be interpreted and dynamically typed. If it's an expression in the process of being compiled, it can be simplified to (sqrt 1) and thence to 1.

car should return the type of the elements of the list it is supplied with, whatever that is. E.g. if x has type (List (List Int)), (car x) should return (List Int). I did this for Full Metal Jacket (see http://web.onetel.com/~hibou/fmj/interpreter.pdf, section 6).

If something has a variable type (e.g. declared as being of type ?x) its type can be inferred once known. If it's of type Any, its type cannot be inferred more specifically than that. If, instead of the above example, you declared x of type (List Any), the list '(1 2 "hello") could still be bound to it, and the call to car would still be accepted by the compiler, but not the call to sqrt.

> If, instead of the above example, you declared x of type (List Any), the list '(1 2 "hello") could still be bound to it, and the call to car would still be accepted by the compiler, but not the call to sqrt.

(sqrt (car '(1 2 "hello"))

So in this example, since it's a (List Any), in order to get this to work would we cast the Any to be an Int to then put it through sqrt?

(sqrt (int (car '(1 2 "hello")))

Also checked out out FMJ - super interesting. I do like the way you used Prolog's unification as way to describe successful type matching. How far along is your work with FMJ?

> So in this example, since it's a (List Any), in order to get this to work would we cast the Any to be an Int to then put it through sqrt?

I wouldn't recommend you use casting the way it's done in C. It defeats the purpose of having a strong type system if you can change the types like that. Having a function which checks the type and gives an error if it's not the type you expect is, I think, a better approach.

I'm still actively developing Full Metal Jacket. Glad you find it interesting. An interpreter for the basic language is almost complete. I'll soon add to my tutorials (http://web.onetel.com/~hibou/fmj/tutorials/TOC.html) how to do inlining and substitution macros, and how to define new types. Then I'll make my code more robust, possibly add a compiler, and arrange a release on a shared-source licence.

Oh yeah, my mistake - you're totally right. So in this case what type does car output (or how do I write the type definition for car), because it can't output multiple types otherwise I wouldn't be able to check its value at compile time?

And yeah, Full Metal Jacket seemed cool (and it's a great name). Do post it here when you start putting those tutorials up!

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.

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.

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.

Thanks man, this is great.

> since it's the heterogeneous nature that will prevent optimization anyway

That was the part I was wondering about. I wanted to see if it was possible to do compile time type checking on a list where I don't know what element would be inside.

It was less for optimization and more for experimentation. Like I was trying to see if I approached building a Lisp with OCaml type checking - how much of the "Lisp" would I have to trade to get proper HM type inference. No purpose other than for play.

Then, although I assumed it was naturally impossible, figured I'd ask.

So car can work for type cons, and then that returns the element regardless of type since the first part of the cons that is pulled becomes just the element?

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).

Hm, that's what I'm thinking as well. Scala's Any list is probably not the same, but I think with Haskell you can do it if you make a union of types. I just want to see if there are ways to allow type inference while keeping the list flexible and heterogenous as otherwise the Lisp loses power if I need to use functions like (car-int '(1 2 3)) to get an int. Do you know how pattern matching works in the case of matching cars to their respective types.

A sum type (union type) solves the problem by making the list homogeneous. A `car` against such a list would return a member typed as this sum type and it would then need to be extracted (e.g., with pattern matching) to get at the value.

> can't figure out what the type of (car '(x y z))

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.

> We know statically that its car is x, of symbol type.

I'm saying within a statically typed Lisp or when trying to use HM's algorithm w you don't know what type of car of (x y z). The type of "symbol" is not specific enough as what operations will you allow to be run on symbol if you're working in a statically typed Lisp with type inference.

If symbol is a character you can't run a float addition on it, and any attempt to do so should throw an error at compile time.

In the case above, I'm using x, y, and z as substitutes for characters, floating point numbers, integers, etc. I'm trying to see if I can figure out the specific type in compile time rather than runtime.

If we know that L is a list, and that is all we know, we don't know what type (car L) is.

If we know that L holds the value (X Y Z), then we know that the type of (car L) is symbol.

> The type of "symbol" is not specific enough

It absolutely is specific enough. It's a fundamental type in the language.

We just don't know what kind of symbol for certain purposes. If we only know that some object O is a symbol, we don't know whether whether it is self-evaluating (nil, t, keyword symbols in CL) or bindable (any other symbol).

In this particular case, not only do we know that (car L) is of type symbol, we know which symbol!!!

We know the exact identity of the object: it is X.

If we know this at compile time, because L is a quoted list literal, we have the strongest possible information about what it is, even more precise than most type information.

> as what operations will you allow to be run on symbol if you're working in a statically typed Lisp with type inference

If I know that O is a symbol, then we can, for instance, compile the (symbol-name O) operation such that O's type tag isn't checked; however, if there is a special representation for a symbol nil, we have to distinguish that. In this case we know that X isn't nil.

> If symbol is a character

... then you're talking about a completely different language that isn't one of the mainstream Lisps. At best a very oddball dialect.

What Lisp tutorial have you been following?

Perhaps you have confused symbol objects, and the use of a symbol as a variable name (X having a value binding in a given environment, and the value of that binding being a character object).

Oh perhaps I'm not being specific enough. Apologies mate.

> If we know this at compile time, because L is a quoted list literal, we have the strongest possible information about what it is, even more precise than most type information.

By '(x y z) I'm assuming that it's not a quoted list literal but a let's say list generated by a function at compile time. Where x, y, and z could be of different types like ('(2.5 7) 6 "hello"). It's very hypothetical, and the contents of the list generated cannot possibly be known at compile time.

> ... then you're talking about a completely different language that isn't one of the mainstream Lisps. At best a very oddball dialect.

And yes, what I'm talking about is building a toy lisp between an ML language and a Lisp to see how much Lispyness you have to trade off for the static typing and the type inference of an ML language. The definition of oddball!

In OCaml for example which has static typing and type inference you can't just have a "symbol". Even though symbols are a basic part of Lisp, you can't have really strong type inference for a "symbol" despite it being a fundamental type in the language as for strong type inference you would want to do stuff like have separate operators for adding integers and adding floating point numbers. This is very important for HM's algorithm w, similarly - in that case, car needs to be able to take one type, and return one type for it to comply with algorithm w. I'm trying to see if other people had ever tried implementing something like this.

Anyway, great conversation! I think DonaldFisk helped me out already, but thanks!

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.

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)?

    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)))

AIUI you can't have HLists in languages without higher-kinded types, and H-M becomes incomplete in that case.

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.

Would this perhaps be a better question for StackOverflow?

I hope not. This place is already more like Noob News than Hacker News, and the transition has been very gradual.

That was a bit harsh. I'm saying we should try hard to retain the culture of the site.

It was delightful to see this question pop up on the front page. And of course, what was the top comment but a reminder that the old HN is now firmly "the old HN," rather than "the present HN."

I dont know the old HN (how old exactly?), but what I know is that it has not changed that much in the last ~4 years in my opinion.

Amusingly, that's precisely correct. This was 5 years ago: https://news.ycombinator.com/item?id=2403696

This is just an old guy being cranky for the old days. Maybe with a dash of ineffectual rose-tinted glasses thrown in. It's probably more a reflection of me than of the site.

The feeling you got when you discovered HN a month after pg opened it up was just electric. When it went away, I started scheming to get it back. Then half a decade passed, and now I can't stop wondering whether it was just a fluke of the world. Maybe it can never happen again, and it's therefore ridiculous to expect it to stay. Or maybe pining for the old days is what people have been doing for ten thousand years in spite of all the amazing progress.

I just miss the feeling of sneaking into a secret club where everyone is way smarter than I am. This current thread is way beyond my abilities to even address, but I love to listen to people who can. Then I realized maybe it's beyond everyone's abilities on the site. Realizing that there are really capable people over on SO made me wonder: where are those people? Can I go listen to them talk about really hard technical topics and then ask them questions? You can't really ask questions on SO, since your words will be ruthlessly purged (with good reason); it's pretty much the opposite of a relaxed setting.

All of this is entirely off-topic of course, so it should probably be detached from https://news.ycombinator.com/item?id=10737507 and marked as such.

But the old days existed. It was so weird. Seeing what it was, and then realizing that it went away, and then realizing it never "should" have even happened in the first place... That it was either an accident or a brilliant design... Everything about it is just so weird.

Secret club feelings are one thing, but in terms of HN's content, most things people say about the old days are probably nostalgia bias. Since you pinpointed 5 years ago, I looked up the front page from 6 years ago:

https://web.archive.org/web/20091215131033/http://news.ycomb...

That's surprisingly little different than how HN would look today, except there's arguably more fluff there.

Six years ago $1.5 million in funding was front page news. The numbers have become orders of magnitude larger.

Certainly. The front page was sometimes an issue, but it never got to be a big problem. The comments, though... Those were something special. Pg's in particular. C.f. today vs https://web.archive.org/web/20080506031933/http://news.ycomb...

I remember precisely when the time period ended, because it was so disappointing: https://news.ycombinator.com/item?id=2604359

What was it about the early comments that were so good?

The commenters were happy, for one. Most of life was pretty dull, and it felt like HN was where people came to life. There was less drama; people were less likely to type out a comment due to anger or frustration.

They were also stronger. People felt like they could influence the world, so they didn't spend a lot of time talking about how to do that, or how the world should be. There was more discussion about intellectual pursuits, or just interesting observations about the world.

The comment threads nowadays are pushy. https://news.ycombinator.com/item?id=10748834 This is the opposite of how it felt in the early days, I think. People were more inquisitive, so they were less aggressive.

There is certainly a component of rose-tinted glasses here, though. Most of my feelings are because I was still pretty young. It was almost a decade ago.

Ah, to be clear I'm not opposed to this post. I guess it's a combination of a) surprise at seeing this type of technical question here, and b) being used to this sort of question on StackOverflow. I feel like at least for this type of question in particular, StackOverflow is better equipped to produce and sort out a good answer. But I can certainly see why it might fit on both.

I'd flag this question on StacKOverflow. There's no code and too much opinion in the possible answers and no objectively correct one. It might be ok on Programmers. StackExchange though it would perhaps benefit from more detail. My general feeling is that it's an XY problem...an assumption about the solution is driving the requirement.

Just checked back on this post from yesterday. The reason I didn't pose it to SO is that 1. I still do associate HN with a strong Lisp community. 2. It's more of a question of opinion versus a technical question itself and figured the discussion could be interesting for the site. I also didn't give too much thought as to where I was posting it.

> Would this perhaps be a better question for StackOverflow?

A thousand times no! This was great!