6 ms·

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

119 points by llambda 13y ago

Avshalom 13y ago
I always assumed haskell's type system would eventually just turn into prolog.
- 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 ago
    Isn't what Qi/shen is ?
  - mkehrt 13y ago
    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.
  - jefffoster 13y ago
    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 https://en.wikipedia.org/wiki/Dependent_type
- lmm 13y ago
  Once I started writing a compile-time DI framework in scala I discovered the type system is basically already there.
talles 13y ago
In the github description there is a typo: 'Langauge Features'. A typo on typo's presentation. On purpose? :)
- BoppreH 13y ago
  I submitted a pull request, and just now I noticed other three identical requests. So I submitted a Github feature request to warn on overlapping contributions, probably along with a few others...
marshray 13y ago
Perhaps now C++ will have some company in the club of languages that people mock for having Turing-completeness in their type system.
- Sharlin 13y ago
  A compile-time C++ LISP interpreter I wrote a while ago just for fun: http://pastebin.com/yz4XvYra http://pastebin.com/yz4XvYra (scroll to the bottom for an example). It's a shame that C++ lacks proper support for compile-time strings, but it would be trivial to write a preprocessor turning a string into a list of char literals.
  - swift 13y ago
    Post-C++11 you can work with strings at compile-time using constexpr template functions. IIRC you need something along the lines of this: > template <size_t N> constexpr foo(const char str[N]) { ... } The fact that constexpr strings can't be template parameters boggles the mind.
- justinpombrio 13y ago
  Well, it depends on what you mean by "Haskell's" type system. The standard Haskell type system, as defined by the Haskell 98 spec, is decidable (and hence not Turing complete). Thus Typo uses a number of GHC-specific type system extensions, one of which has "Undecidable" in its name. They're hidden in Prelude.hs. {-# LANGUAGE NoImplicitPrelude #-} {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-} {-# LANGUAGE FlexibleInstances, UndecidableInstances #-} {-# LANGUAGE OverlappingInstances #-} It's very common to use some extensions, but AFAIK pretty rare to use UndecidableInstances. I'm not actually sure what it does.
  - jkarni 13y ago
    http://www.haskell.org/ghc/docs/7.0.1/html/users_guide/type-class-extensions.html#undecidable-instances http://www.haskell.org/ghc/docs/7.0.1/html/users_guide/type-... has a decent explanation.
deleted 13y ago
[deleted]
seliopou 13y ago
Author here. Besides creating Typo as an exercise in implementing a language, it's also the punchline to a seven-year-old joke[1] about implementing RSA in Haskell's type system, which I did: https://github.com/seliopou/typo/blob/master/examples/rsa.typo Hopefully I'll have the time next week to write a blog post explaining how the encoding of functions work, as well as a cool transformation I employed to make the translation simpler than it otherwise would be. Until then, enjoy! [1]: http://article.gmane.org/gmane.comp.lang.haskell.general/13223 http://article.gmane.org/gmane.comp.lang.haskell.general/132...
th0114nd 13y ago
Don't you think an example where the type system has a visible impact would be appropriate? As it is now, none of the examples show anything that doesn't look like vanilla lisp. I think what makes the Haskell type system nice to use is inference along with type assertions. Do you have type assertions, or is the implementation of types behind the scenes until a type mismatch occurs?
- paradoja 13y ago
  I think maybe you misunderstood what the language does. It is compiled not to Haskell itself, but to the type system. No Haskell code is executed when using the interpreter (well, apart from the interpreter's itself), but it is Haskell's types that are... executed? checked? It's as is you made a program using C++ templates, not C++. Here you have some examples (although it requires some knowledge of Haskell): http://www.haskell.org/haskellwiki/Type_arithmetic http://www.haskell.org/haskellwiki/Type_arithmetic
  - th0114nd 13y ago
    I think wishful thinking twisted the title in my head, into reading of a lisp with a type system like Haskell's.
    - paradoja 13y ago
      This may be near your wishes: http://docs.racket-lang.org/ts-guide/ http://docs.racket-lang.org/ts-guide/
adultSwim 13y ago
Oleg is a beast.

119 points by llambda 13y ago

Avshalom 13y ago

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

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 ago
  Isn't what Qi/shen is ?
- mkehrt 13y ago
  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.
- jefffoster 13y ago
  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 https://en.wikipedia.org/wiki/Dependent_type
lmm 13y ago
Once I started writing a compile-time DI framework in scala I discovered the type system is basically already there.

talles 13y ago

In the github description there is a typo: 'Langauge Features'. A typo on typo's presentation. On purpose? :)

BoppreH 13y ago
I submitted a pull request, and just now I noticed other three identical requests. So I submitted a Github feature request to warn on overlapping contributions, probably along with a few others...

marshray 13y ago

Perhaps now C++ will have some company in the club of languages that people mock for having Turing-completeness in their type system.

Sharlin 13y ago
A compile-time C++ LISP interpreter I wrote a while ago just for fun: http://pastebin.com/yz4XvYra http://pastebin.com/yz4XvYra (scroll to the bottom for an example). It's a shame that C++ lacks proper support for compile-time strings, but it would be trivial to write a preprocessor turning a string into a list of char literals.
- swift 13y ago
  Post-C++11 you can work with strings at compile-time using constexpr template functions. IIRC you need something along the lines of this: > template <size_t N> constexpr foo(const char str[N]) { ... } The fact that constexpr strings can't be template parameters boggles the mind.
justinpombrio 13y ago
Well, it depends on what you mean by "Haskell's" type system. The standard Haskell type system, as defined by the Haskell 98 spec, is decidable (and hence not Turing complete). Thus Typo uses a number of GHC-specific type system extensions, one of which has "Undecidable" in its name. They're hidden in Prelude.hs. {-# LANGUAGE NoImplicitPrelude #-} {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-} {-# LANGUAGE FlexibleInstances, UndecidableInstances #-} {-# LANGUAGE OverlappingInstances #-} It's very common to use some extensions, but AFAIK pretty rare to use UndecidableInstances. I'm not actually sure what it does.
- jkarni 13y ago
  http://www.haskell.org/ghc/docs/7.0.1/html/users_guide/type-class-extensions.html#undecidable-instances http://www.haskell.org/ghc/docs/7.0.1/html/users_guide/type-... has a decent explanation.

deleted 13y ago

[deleted]

seliopou 13y ago

Author here. Besides creating Typo as an exercise in implementing a language, it's also the punchline to a seven-year-old joke[1] about implementing RSA in Haskell's type system, which I did: https://github.com/seliopou/typo/blob/master/examples/rsa.typo Hopefully I'll have the time next week to write a blog post explaining how the encoding of functions work, as well as a cool transformation I employed to make the translation simpler than it otherwise would be. Until then, enjoy! [1]: http://article.gmane.org/gmane.comp.lang.haskell.general/13223 http://article.gmane.org/gmane.comp.lang.haskell.general/132...

th0114nd 13y ago

Don't you think an example where the type system has a visible impact would be appropriate? As it is now, none of the examples show anything that doesn't look like vanilla lisp. I think what makes the Haskell type system nice to use is inference along with type assertions. Do you have type assertions, or is the implementation of types behind the scenes until a type mismatch occurs?

paradoja 13y ago
I think maybe you misunderstood what the language does. It is compiled not to Haskell itself, but to the type system. No Haskell code is executed when using the interpreter (well, apart from the interpreter's itself), but it is Haskell's types that are... executed? checked? It's as is you made a program using C++ templates, not C++. Here you have some examples (although it requires some knowledge of Haskell): http://www.haskell.org/haskellwiki/Type_arithmetic http://www.haskell.org/haskellwiki/Type_arithmetic
- th0114nd 13y ago
  I think wishful thinking twisted the title in my head, into reading of a lisp with a type system like Haskell's.
  - paradoja 13y ago
    This may be near your wishes: http://docs.racket-lang.org/ts-guide/ http://docs.racket-lang.org/ts-guide/

adultSwim 13y ago

Oleg is a beast.