4 ms·

Well, I don't know Idris in detail, so you're better off reading the wiki page I linked to, but I will try to explain further. Idris allows you define types wh

Well, I don't know Idris in detail, so you're better off reading the wiki page I linked to, but I will try to explain further. Idris allows you define types whose definition depends on a value - these are called "dependent types". This allows you to define a type such as "a pair of integers, where the second integer is greater than the first". So, in your example, you could define an immutable String type that stores its length as a fixed value. Then, you define a function that accepts a String of length "len", and a Num (or Integer) with a value that must be less than "len". The type signature might look something like this (if I understand the syntax correctly): ngram : String len val => Num (a <= len) => Vect Num String

twblalock 10y ago
A compiled language cannot know what the value of a variable is at compile time, unless the variable is a constant. Therefore, there cannot possibly be a way to avoid the problem I described in my example, unless your program exists in a a closed world where there are no inputs, and the values of all variables are defined before compilation.
- curryhoward 10y ago
  > A compiled language cannot know what the value of a variable is at compile time, unless the variable is a constant. This statement is false. I recommend reading about dependent types, which enable exactly what you claim is impossible. It's true that in every mainstream language, the type system is not powerful enough to reason about types that "depend" on values, such as the type of MxN matrices, sorted lists, prime numbers, etc. But don't limit your sense of what is possible by your experience with mainstream languages; most have rather limited type systems compared to what we know is possible in theory.
- jestar_jokin 10y ago
  Ah, you're referring to the halting problem? You're right, you can't know every possible value. The article I linked actually mentions how Idris approaches the problem: The word "total" invokes the totality checker[0] which will report an error if the function doesn't cover all possible cases or cannot be (automatically) proven to not enter an infinite loop. So, it sounds like if you can't provably account for all possible inputs, the compiler will recognise this and throw an error. How? Magic! (And a solver, feeding your type constraints into the totality checker, I guess...) (Also, bear in mind languages like Haskell use "lazy" or "non-strict" evaluation by default, where values aren't evaluated until they're actually needed; kiiiinda like Streams?) I'm certainly not an expert on Idris, but I imagine dependent typing provides two benefits: 1) The type signature (which is separate from the implementation; kind of like an Interface in Java) can enforce constraints on your implementation. So, if you define a function with type sig of "Int a => Int b => (a + b)", your implementation must ensure that the returned value is equal to the sum of the two inputs. 2) You can look purely at the type signature to understand what a function is doing. Looking at that type signature above, I can see I want to use that function for addition, not multiplication. Anyway, I'm absolutely not doing justice to these ideas (mostly because I'm not well acquainted with the languages). If you're curious at all, I would highly recommend taking a course on functional programming as a minimum; once I realised that names are meaningless in code, you start seeing everything as reducible to very similar type signatures, which makes you yearn for a language that lets you write your boilerplate once, in a polymorphic way (beyond generics). [0] https://en.wikipedia.org/wiki/Termination_analysis https://en.wikipedia.org/wiki/Termination_analysis
  - twblalock 10y ago
    > So, it sounds like if you can't provably account for all possible inputs, the compiler will recognise this and throw an error. How? Magic! (And a solver, feeding your type constraints into the totality checker, I guess...) That would make many practical, real-world programs noncompilable. Any program which accepts data via API calls, or even reads strings from STDIN, cannot know what values are going to be passed to it before it runs. Compilers cannot predict the future.
- chrismonsanto 10y ago
  You are incorrect. Your objection is like looking at a pen-and-paper proof that a program terminates and saying it is invalid because of the halting problem. If you want to read more about this subject, I recommend Adam Chlipala's "Certified Programming with Dependent Types": http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/
  - twblalock 10y ago
    > Your objection is like looking at a pen-and-paper proof that a program terminates and saying it is invalid because of the halting problem. That is a true statement for any program that accepts input, strictly speaking. The halting problem is unsolvable.
    - roywiggins 10y ago
      A one-state machine that immediately halts, will always halt, regardless of the input. The halting problem cannot be solved in general, but some programs can be proven to halt (or not halt). That's how the first few Busy Beaver numbers were found. For something more substantial: a correct program that implements a regular language recognizer will always halt eventually on any input, because it always makes progress and doesn't have any nonterminating loops. It consumes the whole input and stops. The hard part is proving you wrote it correctly, but that's what coq et al are for.
    - chrismonsanto 10y ago
      No, this is not true. Writing a program to check termination proofs is not difficult. Writing a program to construct termination proofs isn't possible in the general case. If someone hands you a formal pen-and-paper proof of termination it is quite possible to check it for correctness. Analogous statements are true for programming in a dependently typed language.
- pka 10y ago
  To explain in simpler terms, what you do is promote values to types first. I.e. when a user enters a string, you have to somehow prove, using formal logic, that n < l. After that, the proof is encoded in the types and you can use functions as ngram above that depend on this proof.

twblalock 10y ago

A compiled language cannot know what the value of a variable is at compile time, unless the variable is a constant. Therefore, there cannot possibly be a way to avoid the problem I described in my example, unless your program exists in a a closed world where there are no inputs, and the values of all variables are defined before compilation.

curryhoward 10y ago
> A compiled language cannot know what the value of a variable is at compile time, unless the variable is a constant. This statement is false. I recommend reading about dependent types, which enable exactly what you claim is impossible. It's true that in every mainstream language, the type system is not powerful enough to reason about types that "depend" on values, such as the type of MxN matrices, sorted lists, prime numbers, etc. But don't limit your sense of what is possible by your experience with mainstream languages; most have rather limited type systems compared to what we know is possible in theory.
jestar_jokin 10y ago
Ah, you're referring to the halting problem? You're right, you can't know every possible value. The article I linked actually mentions how Idris approaches the problem: The word "total" invokes the totality checker[0] which will report an error if the function doesn't cover all possible cases or cannot be (automatically) proven to not enter an infinite loop. So, it sounds like if you can't provably account for all possible inputs, the compiler will recognise this and throw an error. How? Magic! (And a solver, feeding your type constraints into the totality checker, I guess...) (Also, bear in mind languages like Haskell use "lazy" or "non-strict" evaluation by default, where values aren't evaluated until they're actually needed; kiiiinda like Streams?) I'm certainly not an expert on Idris, but I imagine dependent typing provides two benefits: 1) The type signature (which is separate from the implementation; kind of like an Interface in Java) can enforce constraints on your implementation. So, if you define a function with type sig of "Int a => Int b => (a + b)", your implementation must ensure that the returned value is equal to the sum of the two inputs. 2) You can look purely at the type signature to understand what a function is doing. Looking at that type signature above, I can see I want to use that function for addition, not multiplication. Anyway, I'm absolutely not doing justice to these ideas (mostly because I'm not well acquainted with the languages). If you're curious at all, I would highly recommend taking a course on functional programming as a minimum; once I realised that names are meaningless in code, you start seeing everything as reducible to very similar type signatures, which makes you yearn for a language that lets you write your boilerplate once, in a polymorphic way (beyond generics). [0] https://en.wikipedia.org/wiki/Termination_analysis https://en.wikipedia.org/wiki/Termination_analysis
- twblalock 10y ago
  > So, it sounds like if you can't provably account for all possible inputs, the compiler will recognise this and throw an error. How? Magic! (And a solver, feeding your type constraints into the totality checker, I guess...) That would make many practical, real-world programs noncompilable. Any program which accepts data via API calls, or even reads strings from STDIN, cannot know what values are going to be passed to it before it runs. Compilers cannot predict the future.
chrismonsanto 10y ago
You are incorrect. Your objection is like looking at a pen-and-paper proof that a program terminates and saying it is invalid because of the halting problem. If you want to read more about this subject, I recommend Adam Chlipala's "Certified Programming with Dependent Types": http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/
- twblalock 10y ago
  > Your objection is like looking at a pen-and-paper proof that a program terminates and saying it is invalid because of the halting problem. That is a true statement for any program that accepts input, strictly speaking. The halting problem is unsolvable.
  - roywiggins 10y ago
    A one-state machine that immediately halts, will always halt, regardless of the input. The halting problem cannot be solved in general, but some programs can be proven to halt (or not halt). That's how the first few Busy Beaver numbers were found. For something more substantial: a correct program that implements a regular language recognizer will always halt eventually on any input, because it always makes progress and doesn't have any nonterminating loops. It consumes the whole input and stops. The hard part is proving you wrote it correctly, but that's what coq et al are for.
  - chrismonsanto 10y ago
    No, this is not true. Writing a program to check termination proofs is not difficult. Writing a program to construct termination proofs isn't possible in the general case. If someone hands you a formal pen-and-paper proof of termination it is quite possible to check it for correctness. Analogous statements are true for programming in a dependently typed language.
pka 10y ago
To explain in simpler terms, what you do is promote values to types first. I.e. when a user enters a string, you have to somehow prove, using formal logic, that n < l. After that, the proof is encoded in the types and you can use functions as ngram above that depend on this proof.