Bootstrapping a Type System | Hacker News Reader

Bootstrapping a Type System

journal.stuffwithstuff.com

48 pointstosh9 comments

Note that this post is from October 2010, and it appears that the magpie repo[0] hasn't been committed to in over two years. In addition, the static type system was ripped out of the language about six months after this blog post was written[1].

This is understandable, given that the approach to typing seemed pretty ad-hoc, really unsafe, and somewhat incoherent. The whole point of a type system is to say something about the runtime behavior of a program before you actually run it. To actually execute fragments of your program as part of the type checking step, then, sortof defeats the purpose. Not only that, but typing can fail while producing side effects in your system, some of which may be harmful (launching the nukes, etc.) There are some systems that do _abstract_ interpretation at this point, but that is a model of an execution, not an actual execution, and is therefore sound in the sense that it will not perform random mutations in this strange running/not running superposition.

[0]: https://github.com/munificent/magpie [1]: https://github.com/munificent/magpie/commit/58742b0e7f3431c1...

There are plenty of languages which evaluate fragments of your program as part of the checking step. Simple ones are not even that difficult to write.

http://www.andres-loeh.de/LambdaPi/LambdaPi.pdf

Perhaps compare with Julia, which has a dynamic type system, parameterized types, and multimethods. But it's not trying to do static type checking; the types are for performance and runtime checks.

I always find munificent's essays super insightful and entertaining. Perfect weekend reading material.

Somewhat (un)related: check out his book on Game Programming Patterns (http://gameprogrammingpatterns.com/). Great read of software design and patterns (not only for game developers).

It seems to try to use the same language for the "normal" expression as well as type expression. Is this an implementation of dependent types, or something different?

This is a big part of what DT folks love, although only a part. Essentially the argue that we've already written one great language (supposedly), so why bolt a weak language atop it? Why not just use the same one twice?

Of course, now we need a type language and checker for the type language, a higher order type language, and so on and so forth infinitely. You end up with a rammified hierarchy of types (just like we had back in 1910).

So that's all fine and good and doesn't actually require dependent types yet. In this case, Magpie appears to do something called "Type in Type" which is to compress the whole rammified hierarchy into one layer by just asserting that this is the case. It turns out that this is unsound---you can craft ridiculous things like Girard's Paradox to break it---but for "pragmatic" types that's probably not a huge problem. We're already inconsistent because I assume Magpie is Turing complete.

In order to get dependent types you need what's called the "dependent function space" which lets you accept an argument and then have the return type "depend" on both the type of the argument and the value of the argument

    A : Type
    B : Type -> A -> Type
    depend : (x : A) -> B A x

which I don't think is expressed in Magpie.

It would be interesting to compare to Lux [https://github.com/LuxLang/lux/]

I'd love to see the Hindley Milner type system bootstrapped in this language.

Pretty cool.

Reply on news.ycombinator.com