News for hackers. Stuff that matters.
Re:Typo: A programming language that runs in Haskell's type ... by marshray on Wednesday August 07, 2013 @05:22PM (#6175747)
Perhaps now C++ will have some company in the club of languages that people mock for having Turing-completeness in their type system.
Re:Typo: A programming language that runs in Haskell's type ... by justinpombrio on Wednesday August 07, 2013 @06:08PM (#6176012)
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.
Re:Typo: A programming language that runs in Haskell's type ... by jkarni on Wednesday August 07, 2013 @06:19PM (#6176077)
Re:Typo: A programming language that runs in Haskell's type ... by seliopou on Wednesday August 07, 2013 @08:14PM (#6176554)
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.

Re:Typo: A programming language that runs in Haskell's type ... by Dn_Ab on Wednesday August 07, 2013 @07:47PM (#6176440)
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...

Re:Typo: A programming language that runs in Haskell's type ... by Sharlin on Wednesday August 07, 2013 @05:42PM (#6175849)
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.

Re:Typo: A programming language that runs in Haskell's type ... by swift on Wednesday August 07, 2013 @10:12PM (#6176961)
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.