> Does the compiler magically... No. There is no magic. I had trouble understanding dependent types at first, thinking that the compiler was doing something ma

> Does the compiler magically... No. There is no magic. I had trouble understanding dependent types at first, thinking that the compiler was doing something magical, but in fact it's excrutiatingly simple (it has to be, since computers are dumb). > It's not clear that dependent types even are types. In the case of lists and non-empty lists, these can indeed be represented as different types. In particular, a non-empty list is a pair type, containing a value and a list of values, e.g. `(myInt, myListOfInts)`. This represents a non-empty list starting with `myInt` and followed by whatever's in `myListOfInts`. Notice that this must be non-empty, regardless of what's in `myListOfInts` (or if it's empty), since we have the first value right there (`myInt`)! This is a fundamentally different type than a normal, potentially empty list. Normal lists are a sum type (AKA tagged union): they can either be empty (usually represented with the symbol `nil`), or they can be a pair containing a value and another list (usually represented as a function call `cons(myValue, myList)`). Notice that the second possibility for normal lists corresponds exactly to our representation of non-empty lists. We can think of a list as being either empty or a non-empty list. Likewise we can think of a non-empty list as a pair of a value and a list. Now this all seems quite recursive, self-referential and circular (which it is!), but that's just our mental model. When we actually write this down as a program we must be very explicit about what's going on. In particular, we cannot just throw pairs of things together and expect the compiler to figure out that these are lists/non-empty lists/etc. > Does the compiler magically eliminate the 'remove()' method and then add it back when you add some elements? No. You do that, manually, when you change the representation of your data. In particular, we must explicitly choose whether we're making a normal list or a non-empty list, and we must explicitly convert between the two as necessary (there is no magic!). In Idris this might look something like: data List (t : Type) : Type where ListNil : List t ListCons : t -> List t -> List t data NEList (t : Type) : Type where NECons : t -> List t -> NEList t Now we can write functions which deal with a List or with a NEList, but not both, since that would be a type error e.g. "Expected 'List t', got 'NEList t'" (note that we can code to an interface, and there are some interfaces like `Mappable` or `HasLength` which can be implemented by both types, but that's another topic!). > Does a zero-length list offer a different methods than a list that contains some elements? Yes. If we have a non-empty list, we can get its first element (AKA the "head") and we can get a list of any following elements (AKA the "tail"): -- The head function is trivial for NEList neHead : (t : Type) -> NEList t -> t neHead t (NECons x ys) = x -- The tail function is trivial for NEList neTail : (t : Type) -> NEList t -> List t neTail t (NECons x ys) = ys These functions are easy for NEList, but they only work for NEList; we can't pass these a List since that will be a type error. We also can't write a head or tail function for List, since there's no way to handle the Nil case: -- The head function is impossible to write for List, since there's no valid -- return value when we're given Nil lHead : (t : Type) -> List t -> t lHead t (ListCons x ys) = x lHead t ListNil = {-WHAT COULD POSSIBLY GO HERE?-} lTail : (t : Type) -> List t -> List t lTail t (ListCons x ys) = ys lTail t ListNil = {-WHAT MIGHT GO HERE?-} The head function is impossible to write for List, since there's nothing which makes sense for Nil. For the `lTail` function we could actually return `Nil` and that would type check, but it's debatable whether that actually makes sense. > Does the compiler magically eliminate the 'remove()' method and then add it back when you add some elements? No. We do that when we "add elements" using either `ListCons` or `NECons`: if we use the `NECons` we get back an `NEList` which we can pass to functions like `neHead` and `neTail`. If we instead chose to use `ListCons` then we'd get back a normal List, which would give a type error if we tried to use it with `neHead` or `neTail`. Notice that if we used a `ListCons` value, we know what the return values of `lHead` and `lTail` should be. Yet the compiler doesn't know that (it's not magic!), so it doesn't allow us to write such functions. This is what we mean when we say phrases like "convincing the compiler that such-and-such", or that there are "proof obligations to fulfil": the thing we want to do might be perfectly reasonable (e.g. taking the `lHead` of a `ListCons` value) but the compiler forbids it because there appear to be unhandled cases (`ListNil`) and it's too dumb to figure out that they don't apply. The way we "convince" the compiler is to manually rearrange our data into a different form, where we can handle all of the possibilities (like `NEList` which only has the `NECons` case). Notice that we can easily convert an `NEList` into a `List`, if we need to (e.g. to use a function which only works on `List`): -- Some function we might want to use, which we've only defined for List lLength : (t : Type) -> List t -> Int lLength t ListNil = 0 lLength t (ListCons x ys) = 1 + lLength ys -- It's easy to convert an NEList to a List, since NECons contains the arguments -- we need for ListCons neToL : (t : Type) -> NEList t -> List t neToL t (NECons x ys) = ListCons x ys -- We can get the length of an NEList by converting it to a List first neLength : (t : Type) -> NEList t -> Int neLength t ne = lLength (neToL ne) What if we try to "trick" the compiler into taking the head of a List, by first converting a List into an NEList? It turns out to be impossible, precisely because there's no valid (type-correct) value we can use when we've been given ListNil: -- It's impossible to convert a List to an NEList, since there's nothing we can -- use as the first argument of NECons when we only have Nil lToNE : (t : Type) -> List t -> NEList t lToNE t (ListCons x ys) = NECons x ys lToNE t ListNil = NECons {-WHAT COULD GO HERE?-} Nil Notice that the first argument to NECons must have type `t`, but that could be anything since it's one of our arguments! The same goes for the return value of "head" above. Remember that Idris, etc. don't have a "null" value, so there's nothing we could put here (Haskell would let us use "bottom", i.e. a runtime error, but Idris prevents that unless we disable its totality checker). As for going the other way ("eliminate the 'remove()' method"), notice that the second argument of NECons is a List, not an NEList. This means that when we remove an element from a non-empty list (e.g. using `neTail`, or just pattern-matching on an `NECons` value) we get back a List, which we cannot pass to functions which require a non-empty list. Perhaps that List we get back does actually contain some elements. Yet the compiler doesn't know this (it's not magic!), and it certainly has no reason to think so. If we know that the tail of some NEList is actually non-empty, then we need to "convince the compiler" by converting it into an NEList. As we saw above, we cannot do that in general (since not all lists are non-empty!), but we might be able to do so on a case by case basis, i.e. by figuring out the correct value to pass as the first argument of NECons in each specific case.