5 ms·

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 mea

• dexen 16y ago
  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?
  • merijnv 16y ago
    EDIT: HN ate my asterisks 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!
    • jaekwon 16y ago
      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.
      • eru 16y ago
        Have you read the post your are commenting on? Epigram does not even try to be a complete language.
        • deleted 16y ago
          [deleted]
      • jbapple 16y ago
        > 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.
      • deleted 16y ago
        [deleted]
    • neilk 16y ago
      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.
  • merijnv 16y ago
    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...
    • ionfish 16y ago
      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]. [1] http://www.cis.upenn.edu/~bcpierce/tapl/ http://www.cis.upenn.edu/~bcpierce/tapl/ [2] https://gist.github.com/716834 https://gist.github.com/716834
      • stralep 16y ago
        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. http://www.labri.fr/perso/casteran/CoqArt/index.html http://www.labri.fr/perso/casteran/CoqArt/index.html
        • primodemus 16y ago
          Benjamin Pierce has a course on the mathematical theory of programming languages, using the Coq Proof Assistant: http://www.cis.upenn.edu/~bcpierce/sf/toc.html http://www.cis.upenn.edu/~bcpierce/sf/toc.html 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: http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/
  • jbapple 16y ago
    > 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.
• jules 16y ago
  > meaning that when your program compiles it will be guaranteed to behave correctly For very weak notions of "correctly". If my task is to build a factorial function, epigram will not prevent me from writing a fibonacci function.
• jbapple 16y ago
  > 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)
• richhickey 16y ago
  > 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: http://hackage.haskell.org/trac/ghc/query?status=new&status=assigned&status=reopened&group=priority&type=bug&order=id&desc=1 http://hackage.haskell.org/trac/ghc/query?status=new&sta... 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.
  • cynicalkane 16y ago
    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.
    • richhickey 16y ago
      > 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: http://news.ycombinator.com/item?id=2062910 http://news.ycombinator.com/item?id=2062910 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.