Re:Notes on Idris (2017)
by chriswarbo on Thursday June 07, 2018 @06:23PM
(#17260861)
> it's unclear to me why that's any more reasonable than saying that an integer is either zero or a non-zero integer, and those two are different types.
Sure, that's actually very similar to the list case. We can think of natural numbers as being lists of unit/null values (since the only information we can get from such a list is its length; the elements are uninformative). This corresponds to the "peano numerals", sometimes referred to as unary. Imagine we take the definition of `List` above and get rid of the variable `t`, replacing all of its uses with `Null` (a single-element type containing only the value `null`). The first argument to `ListCons` will then have type `Null`, but since we know that's always going to be `null`, we can just drop that argument. Renaming things appropriately, the result is the following:
data Nat : Type where
Zero : Nat
Succ : Nat -> Nat
We can clearly make this into a non-zero natural, in the same way we made non-empty lists: we just define a type that only has "Succ" (stands for "successor", i.e. one-more-than):
data NZNat : Type where
NZSucc : Nat -> NZNat
The only values of NZNat are successors of some Nat, and hence can't be zero.
We can represent integers in a few ways: one way is to use a pair of natural numbers, and treat their difference as the integer (e.g. `(10, 0)` is 10, `(0, 10)` is -10). Personally I prefer to use the following representation:
data Int : Type where
IZero : Int
IPositive : Nat -> Int
INegative : Nat -> Int
`IZero` obviously represents zero, whilst `IPositive` and `INegative` take a natural and represent counting up or down by that amount + 1, i.e. `IPositive 9` is 10, `INegative 9` is -10.
Again, we can drop the `IZero` to get a non-zero integer:
data NZInt : Type where
NZPositive : Nat -> NZInt
NZNegative : Nat -> NZInt
NOTE: It is not the case that we have some integer value, like `3`, and we're trying to think of the "best type" for it. That's putting the cart before the horse. Rather, we don't have any values until we define some types. Let's say we choose to write the above definition of `Int` in our program; after we do that, we can use it to define values like `IPositive (Succ (Succ Zero))`, which represents/behaves-like the integer `3`. Alternatively, we could choose to write down the `NZInt` definition, and use that to define values like `NZPositive (Succ (Succ Zero))` which is a different value, but also represents/behaves-like the integer `3`. We could also choose to write both implementations, in which case we can have multiple representations of numbers (similar to how we can represent numbers with `int`, `float`, `double`, etc. but some have problems).
In other words, we're not asking "given a number like 3, which type should we apply to it?", rather we're asking "which type of numbers should we pick", which depends more on our task than some 'platonic' property of the numbers themselves.
Also note that none of the examples I've given require dependent types at all; they could all be done in Haskell, StandardML, etc. (the list examples use generics AKA parametric polymorphism)
I actually wrote a blog post about these sorts of types (Nat, List, etc.), along with some that use dependent types like "lists of length N", "numbers less than N", "proof that N is less than M", "proof that X is an element of list L", etc. at http://chriswarbo.net/blog/2014-12-04-Nat_like_types.html
> To my thinking, though, tracking this through types at compile time is more work
Oh absolutely! That's why it should be introduced only as needed. A language like Idris allows this stuff, but doesn't require it.
> and possibly also more error-prone, than tracking it by looking at the values at run time
I would say it causes more programmer errors, since there are conversions and stuff to keep track of, but almost all get caught by the compiler. If it's something that you actually want to check specifically then I think it's better to do at compile time; I wouldn't bother for stuff that could just be left for a catch-all exception handler in a main-loop or something.
Sure, that's actually very similar to the list case. We can think of natural numbers as being lists of unit/null values (since the only information we can get from such a list is its length; the elements are uninformative). This corresponds to the "peano numerals", sometimes referred to as unary. Imagine we take the definition of `List` above and get rid of the variable `t`, replacing all of its uses with `Null` (a single-element type containing only the value `null`). The first argument to `ListCons` will then have type `Null`, but since we know that's always going to be `null`, we can just drop that argument. Renaming things appropriately, the result is the following:
We can clearly make this into a non-zero natural, in the same way we made non-empty lists: we just define a type that only has "Succ" (stands for "successor", i.e. one-more-than): The only values of NZNat are successors of some Nat, and hence can't be zero.We can represent integers in a few ways: one way is to use a pair of natural numbers, and treat their difference as the integer (e.g. `(10, 0)` is 10, `(0, 10)` is -10). Personally I prefer to use the following representation:
`IZero` obviously represents zero, whilst `IPositive` and `INegative` take a natural and represent counting up or down by that amount + 1, i.e. `IPositive 9` is 10, `INegative 9` is -10.Again, we can drop the `IZero` to get a non-zero integer:
NOTE: It is not the case that we have some integer value, like `3`, and we're trying to think of the "best type" for it. That's putting the cart before the horse. Rather, we don't have any values until we define some types. Let's say we choose to write the above definition of `Int` in our program; after we do that, we can use it to define values like `IPositive (Succ (Succ Zero))`, which represents/behaves-like the integer `3`. Alternatively, we could choose to write down the `NZInt` definition, and use that to define values like `NZPositive (Succ (Succ Zero))` which is a different value, but also represents/behaves-like the integer `3`. We could also choose to write both implementations, in which case we can have multiple representations of numbers (similar to how we can represent numbers with `int`, `float`, `double`, etc. but some have problems).In other words, we're not asking "given a number like 3, which type should we apply to it?", rather we're asking "which type of numbers should we pick", which depends more on our task than some 'platonic' property of the numbers themselves.
Also note that none of the examples I've given require dependent types at all; they could all be done in Haskell, StandardML, etc. (the list examples use generics AKA parametric polymorphism)
I actually wrote a blog post about these sorts of types (Nat, List, etc.), along with some that use dependent types like "lists of length N", "numbers less than N", "proof that N is less than M", "proof that X is an element of list L", etc. at http://chriswarbo.net/blog/2014-12-04-Nat_like_types.html
I also wrote a blog post based on another long-winded HN comment I made about dependent types ;) http://chriswarbo.net/blog/2017-11-03-dependent_function_typ...
> To my thinking, though, tracking this through types at compile time is more work
Oh absolutely! That's why it should be introduced only as needed. A language like Idris allows this stuff, but doesn't require it.
> and possibly also more error-prone, than tracking it by looking at the values at run time
I would say it causes more programmer errors, since there are conversions and stuff to keep track of, but almost all get caught by the compiler. If it's something that you actually want to check specifically then I think it's better to do at compile time; I wouldn't bother for stuff that could just be left for a catch-all exception handler in a main-loop or something.