To take as an example Epigram (also mentioned in the blog post). Epigram is not Turing complete, as such the language can be made strongly terminating. This means all programs are guaranteed to terminate (no Halting problem) programs are also strongly (and statically typed) meaning that when your program compiles it will be guaranteed to behave correctly (barring hardware malfunction). Essentially this means we have made the large majority of bugs impossible to be made in this language.
Of course creating a trivial language that is strongly terminating and statically typed is pretty easy. What Epigram is attempting to do is trying to add enough flexibility to create all programs we care about. Not being Turing complete we can't, by definition, create all programs. Of course if we can make all programs we want to make, the inability to create all programs is irrelevant.
Now you might not think these benefits make a language superior to other languages, but I (and the blog post writer as well) do. As he mentions in post adding the ability to lessen these guarantees (i.e. make the languages more dynamic on request) then we have all upsides (less bugs!) and no downsides. Since we can adjust our guarantees down to be less strict and provide more freedom as requested. Lisp can't do the same in reverse as adding the same static guarantees to Lisp is a beyond Herculean task.
> Essentially this means we have made the large majority of bugs impossible to be made in this language
Oh, please. Such a statement ignores the actual kinds of bugs that plague real complex systems. The abilities of static type systems to prevent bugs is dramatically overstated. Consider this:
Now, we all have our bugs, and this is not to beat up on Haskell for having them, but presumably they use their own tools to the greatest extent possible to ensure correctness. What type system is remotely close to being able to help prevent the kinds of bugs in this list? None, and none will any time soon. Because the biggest problems in software are problems of misconception - we've (usually correctly) implemented an incomplete or incorrect idea!
Type systems focus on solving the problems we can solve. Unfortunately, they're not the problems we have.
I spent 2 days last week hunting a bizarre bug that turned out to be ultimately due to a type ambiguity in how JDBC maps Java types to Oracle types. Admittedly this is not a language issue (well, it is on a deeper level), but it's the same sort of problem.
I don't know how much time I've lost in Java to checking, catching, and debugging stupid RuntimeExceptions that would easily be fixed by having a good type system, or writing idiotic boilerplate design patterns that you simply would not have to write if you had a good type system (or were using Clojure).
No language in the world will save you from having to think about your program's desired behavior, but that doesn't mean we should make it hard on ourselves to even implement the behavior we think we want.
> No language in the world will save you from having to think about your program's desired behavior, but that doesn't mean we should make it hard on ourselves to even implement the behavior we think we want.
Therein lies the rub. Is there no cost to static typing? Is it not complex? Is it sufficiently expressive? Does it never make it harder to implement the behavior we think we want?
Should everyone write everything in every program in as provable a way as possible? If not, why not?
As the example here shows, there is a cost in effort expended and complexity:
I'm quite glad people are working on these things, and they have genuine benefits. But to overstate the benefits and ignore the costs (as did the post to which I replied) is not productive.
>Does it never make it harder to implement the behavior we think we want?
I should ask why you're aiming at "never"? I prefer to quantify "how often it makes writing harder". It is more useful.
I think that types could make writing behaviour we want even easier. For example, you could use "session types" and be sure that your routers always understand each other. You can write complex algorithm while establishing its complex invariants in types and be sure you're correct.
I agree that this won't solve all bugs, maybe not even the majority. But I am convinced it solves a significant amount of bugs. Personally I find that an expressive type system can aid significantly in discovering your own misconceptions and clarifying what you intend to do.
When coding Haskell I tend to start by envisioning the type I need my program to have and then fill the code from there.
If the Epigram is not Turing complete, then what kind of programs cannot be expressed in it?
Is the aim of the developer to add TC at some point, or is it a deliberate design choice to remain non-TC?
By the way, I am currently doing a literature study into type theory for my study and I was annoyed by the lack of introduction material for programmers wanting to learn more about it. I've been thinking of writing a "Type theory from first principles for dummies" but I was unsure how much interest there'd be in something like that. If you (or other people here on HN) would be interested in that let me know...
I think that would be a very valuable article. Right now people are basically stuck with TAPL [1], which (while being a fantastic book) is pretty meaty and not exactly cheap. I've been examining the type theory literature myself over the last couple of months (admittedly more from a mathematical angle than a programming one), and there is definitely a dearth of good introductory material. Girard's Proofs and Types is a great book, but it's not easy going and doesn't have a huge amount of direct relevance to programmers. In case anyone else is interested (merijnv, I assume you've glanced at all of these) I have a small bibliography of type theory books [2].
I'm also currently interested in this area, and I would recommend Interactive Theorem Proving and Program Development. At the same time, it is practical and theoretical.
Adam Chlipala's 'Certified Programming With Dependent Types' is a textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation:
> If the Epigram is not Turing complete, then what kind of programs cannot be expressed in it?
I think one quick answer for questions like this is "an interpreter for $LANGUAGE". The reason is that, for a language in which all programs terminate, a type-checked program is a proof that the algorithm terminates. Thus, an interpreter for $SOMEPL in $LANGUAGE is a proof that there is an interpreter for $SOMEPL that terminates on all input.
If $SOMEPL is $LANGUAGE, you get a Goedel/Halting-problem problem.
This is all, of course, assuming that "interpreter" means "function taking as input a valid program and outputting some finite data containing its normalized form". If you define an interpreter to just be a function that performs one step of evaluation, you can get away with it.
Disclaimer: This post contains broken pseudo syntax and pseudo type theory, feel free to make corrections if you are smarter then me.
Epigram (as of yet) is not truly aimed at being a practical language in the hacker sense. It is a research vehicle trying to establish a practical type theory for programming in (i.e. trying to find the sweet spot of how much freedom we require to write useful programs). My knowledge of the underlying theory is still somewhat limited so I don't dare say which programs cannot be written in it.
I would say the lack of Turing completeness is a deliberate design choice. Turing completeness and strong termination are mutually exclusive. Introducing Turing completeness automatically means introducing the Halting problem.
As mentioned in the blog post (one of) the theories behind Epigram is "dependent typing". I agree with the writer that this will be the most exciting thing in programing since...well, ever. What does dependent typing mean? It means the type of a function can depend on the values of the input. To abstract? Let's see if I can clarify:
Haskell currently supports types depending on types (note a lot of this won't be actual valid Haskell, but use pseudo-Haskell syntax), a classical example being the polymorphic list:
data List a = Nil | Cons a (List a)
This is a type which depends on another type. We have "List a" for any given type a. Canonically the type of a type is called * . That is 1:Int meaning "1 has type Int" and Int:* meaning "Int has type * ". Then what is the type of List? It is of course "forall a : * . * " which you could interpret as a function taking a type and returning a new type List :: * -> * .
However, this is not flexible enough to describe somethings we want to be able to describe. For example in Haskell we have the function "head" returning the first item in a list:
head :: [a] -> a
head (x:xs) = x
Now, this function has a problem. What to do when we call head with the empty list as argument? Haskell right now throws an exception, but the compiler should know how long a given list is and it should know that we cannot call head on a list of length 0.
Whatever shall we do? We could painstakingly verify we never call head on a list of length 0 by hand. But we programmers are lazy and hate doing these things. We could waste our lives writing TDD tests with 100% coverage to ensure we never accidentally call head with an empty list, but as lazy programmers we are also to lazy to do this. If only we could make the type of a list depend on its value, thus encoding in the type system whether calling "head" with any given list was safe or not.
Dependent types to the rescue! As mentioned earlier with dependent types the type of a list can depend on a value. Haskell as yet does not support this (partial lie, Haskell has some limited dependent typing support). In Haskell I could not say:
data List a n = Empty | Cons a (List a n-1)
However, in a dependently typed language such a definition is in fact possible. The type of List would then be something like List :: * -> Int -> * . We can then redefine head to have a type that only accepts lists of type "List a n" where n > 0. This means that passing a list which potentially has n == 0 is a type error.
The compiler will at compile time verify that in your code it is never possible that you pass a list with length 0 to head. If it is possible this is a type error and your program will not compile, if it is not possible we have no effectively eliminated the possibility of an empty list exception form our program, without any tedious manual testing. Yay for science!
Thought 1 - but doesn't that mean you immediately run up against the halting problem? Surely we could create a type representing Program, and a function 'halts'. No compiler is going to be able to tell us which programs halt.
Thought 2 - Aha, is this the reason why the language isn't turing complete, so we KNOW that we never run into that difficulty? In other words, the language is constrained somewhat so that we can do these dependent types, because we can then guarantee there's always some calculation the compiler can do ahead of time to ensure all cases will work.
You are correct in the sense that the language isn't Turing complete to guarantee that the language is strongly terminating. The language being strongly terminating means that 1) there is a Normal Form for the type of an expression and 2) the number of steps to reach Normal Form is finite. All programs definable in Epigram have a normal form (i.e. result) and this normal form (result) is reachable in finite time. Therefore hanging and infinite loops are impossible.
However, these aspects are unrelated to the fact that Epigram is dependently typed. We could easily implement a Turing complete dependently typed language or implement a non-dependently typed language which is not Turing complete.
I'm not entirely sure what the problem is you are thinking of in thought 1. Could you elaborate?
It seems to me that it would be possible to create a NonEmptyList type in any language simply by inheriting the regular List type and making sure the constructor and the mutators (if any) enforce the non empty constraint. Presumably a language that supports dependent typing would make the definition of such a type easier (I'm not familiar with any language that supports dependent typing).
However, the problem I see with that kind of fine grained typing is that you would have to convert types in many places as many lists that have to be non empty in one place might be naturally empty in other places. If that is the case, the potential defect is just moved to some other part of the code.
For any given Haskell Compiler I would think that I can construct a program where the Haskell Compiler won't be able to determine, in polynomial time, whether the list has length 0 or not.
> For any given Haskell Compiler I would think that I can construct a program where the Haskell Compiler won't be able to determine, in polynomial time, whether the list has length 0 or not.
Ok, sure, but in total languages (that is, languages in which all functions are total), compilers generally don't just continue running if they can't figure out that some list you've applied "head" to is non-empty. They generally exit with a type error, complaining that you haven't proven that your list is non-empty.
> when your program compiles it will be guaranteed to behave correctly
This is only true if you give your program a strong enough type, and giving your program a stronger type may make it harder to write.
For instance, here is a 14-line version of insertion in red-black trees, due to Okasaki:
data Color = Pink | Gray
data RBT a = Emp | Full Color (RBT a) a (RBT a)
insertRB x s = makeBlack (ins s)
where ins Emp = Full Pink Emp x Emp
ins (Full color a y b) | x < y = balance color (ins a) y b
| x == y = Full color a y b
| x > y = balance color a y (ins b)
makeBlack (Full _ a y b) = Full Gray a y b
balance Gray (Full Pink (Full Pink a x b) y c) z d = Full Pink (Full Gray a x b) y (Full Gray c z d)
balance Gray (Full Pink a x (Full Pink b y c)) z d = Full Pink (Full Gray a x b) y (Full Gray c z d)
balance Gray a x (Full Pink (Full Pink b y c) z d) = Full Pink (Full Gray a x b) y (Full Gray c z d)
balance Gray a x (Full Pink b y (Full Pink c z d)) = Full Pink (Full Gray a x b) y (Full Gray c z d)
balance color a x b = Full color a x b
I munged the names a bit so it can be put in the same module as the code below: the same algorithm, but in a way that ensures that the balance conditions are met. This is 95 lines:
{-# LANGUAGE GADTs, ExistentialQuantification, EmptyDataDecls, StandaloneDeriving #-}
data Z
data S n
data R
data B
data Tree count color a where
Nil :: Tree Z B a
Red :: Tree n B a ->
a ->
Tree n B a ->
Tree n R a
Black :: Tree n lc a ->
a ->
Tree n rc a ->
Tree (S n) B a
--deriving instance Show a => Show (Tree n c a)
data High n a = forall c . High (Tree n c a)
data Set a = forall n . Set (Tree n B a)
--deriving instance Show a => Show (Set a)
data T n c a where
N :: T Z B a
R :: Tree n cl a ->
a ->
Tree n cr a ->
T n R a
B :: Tree n cl a ->
a ->
Tree n cr a ->
T (S n) B a
data H n a = forall c . H (T n c a)
lbbalance :: H n a -> a -> Tree n c a -> High (S n) a
lbbalance (H (R (Red a b c) d e)) f g = High $ Red (Black a b c) d (Black e f g)
lbbalance (H (R a b (Red c d e))) f g = High $ Red (Black a b c) d (Black e f g)
lbbalance (H (R a@Black{} b c@Black{})) d e = High $ Black (Red a b c) d e
lbbalance (H (R Nil b Nil)) d e = High $ Black (Red Nil b Nil) d e
lbbalance (H (B a b c)) d e = High $ Black (Black a b c) d e
lbbalance (H N) a b = High $ Black Nil a b
rbbalance :: Tree n c a -> a -> H n a -> High (S n) a
rbbalance a b (H (R (Red c d e) f g)) = High $ Red (Black a b c) d (Black e f g)
rbbalance a b (H (R c d (Red e f g))) = High $ Red (Black a b c) d (Black e f g)
rbbalance a b (H (R c@Black{} d e@Black{})) = High $ Black a b (Red c d e)
rbbalance a b (H (R Nil c Nil)) = High $ Black a b (Red Nil c Nil)
rbbalance a b (H (B c d e)) = High $ Black a b (Black c d e)
rbbalance a b (H N) = High $ Black a b Nil
lrbalance :: High n a -> a -> Tree n B a -> T n R a
lrbalance (High (Red a b c)) d e = R (Red a b c) d e
lrbalance (High (Black a b c)) d e = R (Black a b c) d e
lrbalance (High Nil) a b = R Nil a b
rrbalance :: Tree n B a -> a -> High n a -> T n R a
rrbalance a b (High (Red c d e)) = R a b (Red c d e)
rrbalance a b (High (Black c d e)) = R a b (Black c d e)
rrbalance a b (High Nil) = R a b Nil
hhigh :: High n a -> H n a
hhigh (High Nil) = H N
hhigh (High (Red a b c)) = H (R a b c)
hhigh (High (Black a b c)) = H (B a b c)
insertTree :: Ord a => a -> Set a -> Set a
insertTree x (Set y) =
case insert x y of
H N -> Set Nil
H (R a b c) -> Set (Black a b c)
H (B a b c) -> Set (Black a b c)
insert :: Ord a => a -> Tree n c a -> H n a
insert x y@Nil = hhigh $ insertBlack x y
insert x y@Red{} = H $ insertRed x y
insert x y@Black{} = hhigh $ insertBlack x y
insertRed :: Ord a => a -> Tree n R a -> T n R a
insertRed x (Red l c r) =
case compare x c of
LT -> lrbalance (insertBlack x l) c r
EQ -> R l c r
GT -> rrbalance l c (insertBlack x r)
insertBlack :: Ord a => a -> Tree n B a -> High n a
insertBlack x Nil = High $ Red Nil x Nil
insertBlack x (Black l y r) =
case compare x y of
LT -> lbbalance (insert x l) y r
EQ -> High $ Black l x r
GT -> rbbalance l y (insert x r)
I agree that this is only true when the language is given a strong enough type and that giving such a type may be to cumbersome. In fact languages that can do most of these things already exist (Coq and Agda for example) but they are indeed to cumbersome.
That is why we need people experimenting with new languages like Epigram, attempting to find a way of writing these programs in such a way that these strong types don't become to cumbersome.
These strong types will always be somewhat cumbersome, because they are the proof that your program is correct in certain respects, and non-trivial proofs are not free. When you hear someone use the phrase "correct by construction," you should ask you do when you accidentally construct the wrong thing. I'm afraid the answer is that you "correct by reconstruction."
Of course creating a trivial language that is strongly terminating and statically typed is pretty easy. What Epigram is attempting to do is trying to add enough flexibility to create all programs we care about. Not being Turing complete we can't, by definition, create all programs. Of course if we can make all programs we want to make, the inability to create all programs is irrelevant.
Now you might not think these benefits make a language superior to other languages, but I (and the blog post writer as well) do. As he mentions in post adding the ability to lessen these guarantees (i.e. make the languages more dynamic on request) then we have all upsides (less bugs!) and no downsides. Since we can adjust our guarantees down to be less strict and provide more freedom as requested. Lisp can't do the same in reverse as adding the same static guarantees to Lisp is a beyond Herculean task.