Typo: A programming language that runs in Haskell's type system

Re:Typo: A programming language that runs in Haskell's type ... by jkarni on Wednesday August 07, 2013 @06:15PM (#6176050)

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/

[ Parent | on HN ]

Re:Typo: A programming language that runs in Haskell's type ... by mkehrt on Wednesday August 07, 2013 @08:40PM (#6176646)

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.

[ Parent | on HN ]

Re:Typo: A programming language that runs in Haskell's type ... by jefffoster on Thursday August 08, 2013 @04:27AM (#6177840)

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

[ Parent | on HN ]

Re:Typo: A programming language that runs in Haskell's type ... by agumonkey on Wednesday August 07, 2013 @07:45PM (#6176432)

Isn't what Qi/shen is ?

[ Parent | on HN ]