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

https://github.com/seliopou/typo

by llambda • 13 years ago

119 21 13 years ago

github.com

talles• 13 years ago

In the github description there is a typo: 'Langauge Features'.

A typo on typo's presentation. On purpose? :)

BoppreH• 13 years 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...

Avshalom• 13 years ago

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

jkarni2• 13 years 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 [2]http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/about/

agumonkey• 13 years ago

Isn't what Qi/shen is ?

mkehrt• 13 years 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• 13 years 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

lmm• 13 years ago

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

marshray• 13 years 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• 13 years ago

A compile-time C++ LISP interpreter I wrote a while ago just for fun: 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• 13 years 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• 13 years 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.

jkarni2• 13 years ago

http://www.haskell.org/ghc/docs/7.0.1/html/users_guide/type-... has a decent explanation.

Dn_Ab• 13 years ago

There is nothing inherently bad with turing complete type systems aka allow powerful logic but aren't total (there are ways to avoid proof inconsistency). Other than the risk of non terminating type checking/compilation, the issue is a matter of difficulty (hard to do right) not principle (bad to do).

The problem with C++ templates is not that they are turing complete. Versus Haskell, it is the difference between one day waking up and finding out that layer upon layer of unspeakable ad-hocery have suddenly yielded a deranged spam bot suffering from a severe case of logorrhea that can pass the turing test, given a patient examiner.. And an AI designed from first principles using an elegant theory - even if messy in implementation from unforeseen expectations requiring a patchwork of (still principled) extensions.

An approachable language with a particularly interesting type system that compiles to prologish: http://www.shenlanguage.org/learn-shen/types/types_sequent_c...

seliopou2• 13 years 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/132...

th0114nd2• 13 years 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?

paradoja2• 13 years 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

th0114nd2• 13 years ago

I think wishful thinking twisted the title in my head, into reading of a lisp with a type system like Haskell's.

adultSwim• 13 years ago

Oleg is a beast.

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

Related Stories