Typo: A programming language that runs in Haskell's type system | Hacker News Reader

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

github.com

119 pointsllambda21 comments

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...

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.

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?

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

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

This may be near your wishes: http://docs.racket-lang.org/ts-guide/

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

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.

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.

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.

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

UndecidableInstances a.k.a. YouDecidableInstances.

While I was writing the Prelude, I messed up one of the definitions and ghc kept blowing the context stack limit. So I tried it with -fcontext-stack=5000, figuring it wasn't my bug but just a consequence of the inefficient encoding I was using. The type system ended up allocating upwards of 4 gigs before I killed it.

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...

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

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

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...

Oleg is a beast.

Reply on news.ycombinator.com