7 ms·

Regarding nulls, have a look at how Haskell deals with nulls. The basic idea is that any nullable value gets wrapped in a "Maybe", and you use pattern matching

Regarding nulls, have a look at how Haskell deals with nulls. The basic idea is that any nullable value gets wrapped in a "Maybe", and you use pattern matching to handle the case of missing/empty values. This is much more explicit than null values in Java, where any object could be null at any time, and actually leads to cleaner code (i.e. to avoid lots of "Maybe" boilerplate, you can match for "Nothing" and return a default value as soon as possible to first matching "Nothing"). Regarding illegal arguments, have a look at something like Idris, which has a type system with "dependent types". The Wikipedia page has an example[0]; types can have values, so you can express a "pairAdd" function that accepts two vectors, each vector requiring the same length. I guess "types" and "compile-time checks" are sometimes used interchangeably. I absolutely think tools (such as compilers) should be leveraged to provide as much assistance as possible; whether that comes in the form of types, or some other mechanism that resembles types. [0] https://en.wikipedia.org/wiki/Idris_(programming_language)#Dependent_types https://en.wikipedia.org/wiki/Idris_(programming_language)#D...

twblalock 10y ago
How would Idris provide a solution to the situation in my example?
- jestar_jokin 10y ago
  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
- joel_ms 10y ago
  Probably with a function with a type signature something like this (which is in Agda, another dependently typed language, but the idea holds): nGram : {l : Nat}{n : Fin l} -> Vec l Char -> n -> List (Vec n Char) To break it up: "nGram" is the name of the function "{l : Nat}" means l is a natural number "{n : Fin l}" means n is a finite number smaller than l "Vec l Char" is the first argument, declared as a vector of characters, with length l "n" is the second argument (previously declared as a finite number smaller than l) "List (Vec n Char)" is the return type, a list which consists of vectors of characters where each vector is of length n For an explanation on how and why this works you can check out these papers: http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWo... The first is more about programming in Agda while the second goes into how dependently typed languages relate to logic. Together they provide sufficient definitions of Nat, Fin, Vec and List to declare the nGram function. If you're unfamiliar with ML-style syntax the above definiton probably looks weird, but can be written in a pseudo-java style like this: List<Vec<N,Char>> nGram<Nat L,Fin<L> N>(Vec<L,Char> input_string, N n){}
  - twblalock 10y ago
    This makes no sense. No language can know the value of a variable at compile time, unless that variable is a constant. If the function you have defined is passed a string s and an int n, where n is greater than len(s), there is no way the compiler can know that will happen in advance. It will be a runtime error. IllegalArgumentException is also a runtime error. You have not solved anything.
    - curryhoward 10y ago
      Actually, joel_ms is correct; you can encode these "dynamic" properties of values in a static type system, in the same way that you can prove properties about a program on paper without actually running it. The connection between programs and proofs [1] is rather mind-blowing to learn about, and unfortunately no popular programming language supports this style of "certified" programming. But there are some interesting languages which do, such as Idris and Coq. [1] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
XorNot 10y ago
I've never really grokked the improvement this is supposed to represent. It's a slightly more explicit class of return codes I guess, and feels an awful lot like exceptions as well. Go for example, half-straddles this world too. I can half-see the benefit of being able to know if something produces an error term (annoying in Python when you're trying to be thorough with exception handling) but conversely there's so few situations I encounter where a function can't error that it's practically irrelevant - what does it matter to me that some set of functions can't throw, if every bit of IO, network and disk before them can and will at some point?
twblalock 10y ago
So instead of checking if a variable is null, I have to check if the variable is a Maybe type, and if it contains a value. I hope you can see how this is pretty much the same as checking if a variable is null. It takes just as much work, and has the same outcome.
- majewsky 10y ago
  No. When you get passed a "Foo", you know for a fact that it's non-null. When you get passed a "Maybe Foo", you know for a fact that there are intentional cases where this thing will be null. In Java, you just have one type for both purposes, so you end up checking non-nullness every time (or just blindly rely on non-nullness having been checked elsewhere before).
- jestar_jokin 10y ago
  Not as such; functional languages use "pattern matching", so you are forced to match each possible outcome. This way, it explicitly brings the issue of nulls out into the open; if you have a Maybe it might be null, if you have a String, or Number, or anything else, it is never null! This means the language allows you to define areas of your program that are null-safe, and areas where nulls are expected. Compare to languages where you must remember to check null on every use of a null variable. I guarantee I can pick any Java codebase and find a method where arguments to that method, or a class's properties, are not checked for null on every use. How do I know that the use is safe? Usually by coding conventions; maybe immutable instances represented by values set only in a constructor, although what's to stop null being passed in?
- lkitching 10y ago
  90% of the time you don't need to check the value for null, because it won't be null and that will be reflected in the type. In langauges where all types contain null, there is no way for a function to communicate that it always returns a non-null value, which forces the caller to make redundant checks. If the value can be null, then they are at risk of NullReferenceExceptions if they fail to check. In cases where the value could be missing, the type is change to Maybe and the caller is forced to handle the null case. They can still avoid explicit checks using various combinators (>>=, fmap, liftA2 etc.) which propagate empty Maybe values. Explicit matching on Maybe is fairly uncommon in languages which support it.

twblalock 10y ago

How would Idris provide a solution to the situation in my example?

jestar_jokin 10y ago
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
joel_ms 10y ago
Probably with a function with a type signature something like this (which is in Agda, another dependently typed language, but the idea holds): nGram : {l : Nat}{n : Fin l} -> Vec l Char -> n -> List (Vec n Char) To break it up: "nGram" is the name of the function "{l : Nat}" means l is a natural number "{n : Fin l}" means n is a finite number smaller than l "Vec l Char" is the first argument, declared as a vector of characters, with length l "n" is the second argument (previously declared as a finite number smaller than l) "List (Vec n Char)" is the return type, a list which consists of vectors of characters where each vector is of length n For an explanation on how and why this works you can check out these papers: http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWo... The first is more about programming in Agda while the second goes into how dependently typed languages relate to logic. Together they provide sufficient definitions of Nat, Fin, Vec and List to declare the nGram function. If you're unfamiliar with ML-style syntax the above definiton probably looks weird, but can be written in a pseudo-java style like this: List<Vec<N,Char>> nGram<Nat L,Fin<L> N>(Vec<L,Char> input_string, N n){}
- twblalock 10y ago
  This makes no sense. No language can know the value of a variable at compile time, unless that variable is a constant. If the function you have defined is passed a string s and an int n, where n is greater than len(s), there is no way the compiler can know that will happen in advance. It will be a runtime error. IllegalArgumentException is also a runtime error. You have not solved anything.
  - curryhoward 10y ago
    Actually, joel_ms is correct; you can encode these "dynamic" properties of values in a static type system, in the same way that you can prove properties about a program on paper without actually running it. The connection between programs and proofs [1] is rather mind-blowing to learn about, and unfortunately no popular programming language supports this style of "certified" programming. But there are some interesting languages which do, such as Idris and Coq. [1] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

XorNot 10y ago

I've never really grokked the improvement this is supposed to represent. It's a slightly more explicit class of return codes I guess, and feels an awful lot like exceptions as well. Go for example, half-straddles this world too. I can half-see the benefit of being able to know if something produces an error term (annoying in Python when you're trying to be thorough with exception handling) but conversely there's so few situations I encounter where a function can't error that it's practically irrelevant - what does it matter to me that some set of functions can't throw, if every bit of IO, network and disk before them can and will at some point?

twblalock 10y ago

So instead of checking if a variable is null, I have to check if the variable is a Maybe type, and if it contains a value. I hope you can see how this is pretty much the same as checking if a variable is null. It takes just as much work, and has the same outcome.

majewsky 10y ago
No. When you get passed a "Foo", you know for a fact that it's non-null. When you get passed a "Maybe Foo", you know for a fact that there are intentional cases where this thing will be null. In Java, you just have one type for both purposes, so you end up checking non-nullness every time (or just blindly rely on non-nullness having been checked elsewhere before).
jestar_jokin 10y ago
Not as such; functional languages use "pattern matching", so you are forced to match each possible outcome. This way, it explicitly brings the issue of nulls out into the open; if you have a Maybe it might be null, if you have a String, or Number, or anything else, it is never null! This means the language allows you to define areas of your program that are null-safe, and areas where nulls are expected. Compare to languages where you must remember to check null on every use of a null variable. I guarantee I can pick any Java codebase and find a method where arguments to that method, or a class's properties, are not checked for null on every use. How do I know that the use is safe? Usually by coding conventions; maybe immutable instances represented by values set only in a constructor, although what's to stop null being passed in?
lkitching 10y ago
90% of the time you don't need to check the value for null, because it won't be null and that will be reflected in the type. In langauges where all types contain null, there is no way for a function to communicate that it always returns a non-null value, which forces the caller to make redundant checks. If the value can be null, then they are at risk of NullReferenceExceptions if they fail to check. In cases where the value could be missing, the type is change to Maybe and the caller is forced to handle the null case. They can still avoid explicit checks using various combinators (>>=, fmap, liftA2 etc.) which propagate empty Maybe values. Explicit matching on Maybe is fairly uncommon in languages which support it.