4 ms·
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
by jkarni 13y ago
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 http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf
[2]http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/about/ http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/about/
- agumonkey 13y agoIsn't what Qi/shen is ?
- mkehrt 13y agoHindley-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.
- jefffoster 13y agoThis 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 https://en.wikipedia.org/wiki/Dependent_type