7 ms·

Of course you have to subscribe to the idea that this safety and verification is something that's good and superior. I do. Why is it superior? I've alway

by jaekwon 16y ago

Of course you have to subscribe to the idea that this safety and verification is something that's good and superior. I do. Why is it superior? I've always believed that a superior language is one that is as close to natural language as possible. Natural language doesn't have strict type checking, and a great many things were told with 'incorrect' grammar.

coderdude 16y ago
Natural language has ambiguity. That kills its effectiveness as a programming language.
- varjag 16y ago
  It would be interesting to see how many Haskell programmers are also Lojban speakers.
  - Wilfred 16y ago
    Funny you should mention that. There was a survey of favoured web frameworks[1] in the Lojban community, and Haskell with snap won[2]. 1: http://www.surveymonkey.com/s/T6B69LK http://www.surveymonkey.com/s/T6B69LK 2: http://teddyb.org/~rlpowell/public_media/lojban_survey.PNG http://teddyb.org/~rlpowell/public_media/lojban_survey.PNG
- jaekwon 16y ago
  Solvable if the compiler can initiate an intelligent conversation. Like, "What you said is ambiguous. Did you mean? ..."
  - dexen 16y ago
    Do you envision search engines becoming Turing complete at some point in time? ;-)
    - jaekwon 16y ago
      I don't know why you ask that. Are you suggesting that it is difficult to determine whether a statement is ambiguous or not?
      - dexen 16y ago
        It was half-joke, actually -- but there is point to it, to some extent. I was referring to the fact that (web) search engines often display `Did you mean X?' when query string contains a symbol they don't know. Also, in a way, a search engine does interpret the query as a (simplistic) program of sorts. And, once in a while, it'd be handy to be able to issue query to search engines in a more powerful query language... So I saw a weak analogy there, between search engine and a compiler with the `Did you mean X?' feature.
        Swannie 16y ago
        You appear to be confusing "Turing complete" and the "Turing test". These two concepts are only related by the man which proposed them. They are quite separate classes of concept.
  - kleiba 16y ago
    That would be awesome! Perhaps we could have an animated character have that conversation with us... how about an intelligent paperclip or something?! Wouldn't programming become so cool!?!!
    - jaekwon 16y ago
      I hope in 20 years we look back and say 'duh, of course'. And yeah, it would be so cool.
      - thesz 16y ago
        I feel like I should introduce you to Agda2: http://wiki.portal.chalmers.se/agda/pmwiki.php http://wiki.portal.chalmers.se/agda/pmwiki.php You write something, Agda2 checks it and says that you forget something, you wrote an inconsistent code or you wrote ambiguous code (it is possible to hide some parts of code).
merijnv 16y ago
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.
- 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!
srean 16y ago
Natural language is hardly appropriate for things that we use computers for, primarily because of its inherent ambiguity. Its not a language for expressing algorithms, which is precisely what one uses a computer for. If we expect to code in language that is close to natural, we should also expect an error rate of natural systems. But then Dijkstra said it much better: http://www.cs.utexas.edu/users/EWD/transcriptions/EWD06xx/EWD667.html http://www.cs.utexas.edu/users/EWD/transcriptions/EWD06xx/EW...
likpok 16y ago
I recall a story about some programming language which tried hard to correct errors. The programmer wrote 'Hello World' with a minor syntactic error. The program output '7', because it fixed the syntax. If you have ever used Latex, you experience the pain that is the compiler trying to fix your program. The result is a large number of errors with little correspondence to the actual location. Additionally, it seems that a common theme in style guides is to write for the person who is trying to update your code in three years, after the requirements have changed. I would expect that for that you want as much static as possible, as it makes for less state to keep in your head.

by jaekwon 16y ago

coderdude 16y ago

Natural language has ambiguity. That kills its effectiveness as a programming language.

varjag 16y ago
It would be interesting to see how many Haskell programmers are also Lojban speakers.
- Wilfred 16y ago
  Funny you should mention that. There was a survey of favoured web frameworks[1] in the Lojban community, and Haskell with snap won[2]. 1: http://www.surveymonkey.com/s/T6B69LK http://www.surveymonkey.com/s/T6B69LK 2: http://teddyb.org/~rlpowell/public_media/lojban_survey.PNG http://teddyb.org/~rlpowell/public_media/lojban_survey.PNG
jaekwon 16y ago
Solvable if the compiler can initiate an intelligent conversation. Like, "What you said is ambiguous. Did you mean? ..."
- dexen 16y ago
  Do you envision search engines becoming Turing complete at some point in time? ;-)
  - jaekwon 16y ago
    I don't know why you ask that. Are you suggesting that it is difficult to determine whether a statement is ambiguous or not?
    - dexen 16y ago
      It was half-joke, actually -- but there is point to it, to some extent. I was referring to the fact that (web) search engines often display `Did you mean X?' when query string contains a symbol they don't know. Also, in a way, a search engine does interpret the query as a (simplistic) program of sorts. And, once in a while, it'd be handy to be able to issue query to search engines in a more powerful query language... So I saw a weak analogy there, between search engine and a compiler with the `Did you mean X?' feature.
      - Swannie 16y ago
        You appear to be confusing "Turing complete" and the "Turing test". These two concepts are only related by the man which proposed them. They are quite separate classes of concept.
- kleiba 16y ago
  That would be awesome! Perhaps we could have an animated character have that conversation with us... how about an intelligent paperclip or something?! Wouldn't programming become so cool!?!!
  - jaekwon 16y ago
    I hope in 20 years we look back and say 'duh, of course'. And yeah, it would be so cool.
    - thesz 16y ago
      I feel like I should introduce you to Agda2: http://wiki.portal.chalmers.se/agda/pmwiki.php http://wiki.portal.chalmers.se/agda/pmwiki.php You write something, Agda2 checks it and says that you forget something, you wrote an inconsistent code or you wrote ambiguous code (it is possible to hide some parts of code).

merijnv 16y ago

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.

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!

srean 16y ago

Natural language is hardly appropriate for things that we use computers for, primarily because of its inherent ambiguity. Its not a language for expressing algorithms, which is precisely what one uses a computer for. If we expect to code in language that is close to natural, we should also expect an error rate of natural systems. But then Dijkstra said it much better: http://www.cs.utexas.edu/users/EWD/transcriptions/EWD06xx/EWD667.html http://www.cs.utexas.edu/users/EWD/transcriptions/EWD06xx/EW...

likpok 16y ago

I recall a story about some programming language which tried hard to correct errors. The programmer wrote 'Hello World' with a minor syntactic error. The program output '7', because it fixed the syntax. If you have ever used Latex, you experience the pain that is the compiler trying to fix your program. The result is a large number of errors with little correspondence to the actual location. Additionally, it seems that a common theme in style guides is to write for the person who is trying to update your code in three years, after the requirements have changed. I would expect that for that you want as much static as possible, as it makes for less state to keep in your head.