Hacker News Reader

Comment by Avshalom | Hacker News Reader

I always assumed haskell's type system would eventually just turn into prolog.

I've always hoped some language would have a prolog type system. Just today, I was pointed to liquid types [1,2] in haskell-cafe, and they look really promising in that respect. But the idea of having my compiler bail with a nice error message when I try:

fibs = 0 : 1 : zipWith (+) fibs (tail fibs)

fibPlus :: (int LESSTHAN 30) -> (int LESSTHAN 500000) fibPlus x = fibs !! x + 100

Is definitely too good to be true.

[1]http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf [2]http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/about/

Isn't what Qi/shen is ?

Hindley-Milner style type inference, which is done by MLs and is similar to what is done in Haskell, uses unification, which is a large part of how Prolog reasons, to determine if two types with still unknown subparts can be the same. You can do surprisingly complex things in these type systems.

For a more complex type system that does similar things and allows a lot more reasoning in the type system, you could take a look at Agda. This is a Haskell-like language with a fully dependent type system, i.e., types can contain arbitrary language terms. This has the downside of being not-quite-Turing-complete, as you want to be able to decidably typecheck. However, it is powerful enough that its type system is often used to automate proofs about both programming language theory and more ordinary math.

This is my understanding of what dependent types [1] will allow you to accomplish (at least in some imaginary future).

[1] https://en.wikipedia.org/wiki/Dependent_type

Once I started writing a compile-time DI framework in scala I discovered the type system is basically already there.

Reply on news.ycombinator.com