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