3 ms·

What are refinement types and dependent function types?

shakna 9y ago
A refinement type, is a value type with preconditions attached. Simply put, instead of something being an Integer, you can say it is an Integer, but only between 1 and 6. In this case, this should be enforced at compile-time.
alphaalpha101 9y ago
A refinement type is a type along with a predicate (a function that returns a boolean). e.g. 'integer between 1 and 6 inclusive' is a refinement of integer to only the integers that satisfy the predicate 'x => 1 < x <= 6'
chriswarbo 9y ago
Dependent function types allow the return type of a function refer to the argument value of the function. The classic example is "vectors", which are like lists but have a statically-checked length. Here's an example function involving vectors: duplicate : (t : Type) -> t -> (n : Nat) -> (Vector n t) This type signature says that `duplicate` is a function of 3 arguments: `a -> b` means a function from argument type `a` to return type `b`, and `a -> b -> c` can either be interpreted as "a function taking an `a` and returning a `b -> c`" or (equivalently) "a function taking an `a` and a `b` and returning a `c` (see https://wiki.haskell.org/Currying https://wiki.haskell.org/Currying for why this is equivalent). Argument types are written in one of two ways: if they're written like `a` (for example `Int` or `String`), then the type of the argument is `a`; if they're written `a : b` (for example `age : Int`) then the argument type is `b`, but later types can refer to the value as `a`. So this signature says that the first argument of `duplicate` is called `t`, and it is a `Type`. The second argument has type `t`; this means the type of the second argument depends on the value of the first argument: if we call `duplicate` with `Bool : Type` as the first argument, then the second argument must be a `Bool`. The third argument is called `n`, and has type `Nat` (natural numbers: i.e. the positive integers including zero). The return type is `Vector n t`, i.e. a list of length `n` containing elements of type `t`. Note that we're referring to argument values by name, but we don't know what particular value they will be (i.e. which number `n` will be, or which type `t` will be). We can think of `a : b` as being `for all a of type b`. If we think about functions returning lists, like `map` or `reverse`, we can "cheat" by having them always return an empty list; such functions satisfy their type signature (they return a list), but don't behave in the way we want. In contrast, the "for all" nature of dependent function types can be used to prevent this sort of "cheating". The `duplicate` function can't just return an empty vector, since it must return a vector of length `n`, and the implementation must work for all values of `n`. We're forced to write a function which constructs a vector of the correct length: empty when `n` is zero, or non-empty otherwise. To construct a non-empty vector, we need to put a value inside it. What value can we use? We can't "cheat" by using, say, the value `"hello"`, since that would give us a vector containing `String`, whilst our return type forces us to make a vector containing `t`. Whatever our function does, it must work for all values of `t` (`String`, `Bool`, `Int`, `Vector 5 (Int -> Bool)`, etc.). Since we don't know what `t` will be, we can't "invent" a value of the right type. The only thing we can do is use an existing value which will always have type `t`. The only way something can have type `t` is if it appears in our type signature, since that's the scope of the name `t`. The only thing in our type signature which has type `t` is the second argument. Hence we must use the second argument as the elements of our vector (if it's non-empty). One implementation which satisfies this type is the following (assuming that `Nat` is encoded as Peano numerals https://en.wikipedia.org/wiki/Successor_function https://en.wikipedia.org/wiki/Successor_function ): duplicate t x n = case n of zero -> vectorNil t succ m -> vectorCons t x (duplicate t x m) This isn't the only possible implementation, for example we might choose to send the recursive call through a `vectorReverse` function (although it would be pointless), but such differences cannot alter the input/output behaviour of the function. Of course, we don't have to use dependent function types to restrict all of a function's behaviour. If we think back to the `map` example, we take a function of type `a -> b`, a `List a` and must return a `List b`: the easiest thing to do is return an empty list, which satisfies the type but isn't what we want. If we instead make a `vectorMap` function, where `List` is replaced with `Vector n`, then that "cheat" no longer works (since an empty vector doesn't always have length `n`). We could still mess around with the contents, like reversing it or doing some other permutation, but that's harder than just doing the right thing. The path of least resistance is to write a correct implementation!
- fiddlerwoaroof 9y ago
  I like the way Edwin Brady talks about this: a dependently typed language is one in which types are first class. That is, you can use them as values in computations and return them.
  - chriswarbo 9y ago
    "First class types" and "dependent types" are actually two different things. We can have first class types without any dependencies. For example: isEven : Nat -> Type isEven zero = Unit isEven (succ zero) = Empty isEven (succ (succ n)) = isEven n fortyTwoEven : isEven 42 fortyTwoEven = unit Here the `isEven` function calculates a type based on the given number: if the number's even, it returns the `Unit` type, of which there is a value `unit`; if the number's odd, it returns the `Empty` type, of which there are no values. The value `fortyTwoEven` is a "proof" that the number `42` (which would actually be `succ (succ (succ ...))` nested 42 times) is even. The proof is the value `unit`, which will only work if `isEven 42` returns `Unit`, which will only happen if 42 is even, so everything works out. We can write a type like `isEven 43`, but that will return the type `Empty`, which there's no way to satisfy. We can use this sort of thing to do static checks of reasonably simple data; for example, if we have a bunch of config parameters which need to be related in some way. Dependent types add the "naming" part, which we can use in functions (as explained above), but also in other "compound" datastructures like tuples `(n : Nat, isEven n)` and records `{ n : Nat, evenProof : isEven n }` The annoying thing is that few languages seem to have first class types at all, so every explanation of dependent types has to start by introducing first class types, and then explaining the "dependent" parts. It's like trying to explain something like interfaces, if all mainstream languages were dynamically typed. We'd have to begin by explaining what types are, and then go on to explain interfaces. Readers might easily confuse features of types with features of interfaces, which would lead to much confusion. I think that's kind of happened with "dependent types" and "first class types", although I haven't seen any/many systems which have one without the other, so maybe it's not too bad :)
- pmoriarty 9y ago
  That was some of the clearest technical writing I've ever read. I hope you write a book, if you haven't already.

A refinement type, is a value type with preconditions attached. Simply put, instead of something being an Integer, you can say it is an Integer, but only between 1 and 6. In this case, this should be enforced at compile-time.

alphaalpha101 9y ago

A refinement type is a type along with a predicate (a function that returns a boolean). e.g. 'integer between 1 and 6 inclusive' is a refinement of integer to only the integers that satisfy the predicate 'x => 1 < x <= 6'

chriswarbo 9y ago

Dependent function types allow the return type of a function refer to the argument value of the function. The classic example is "vectors", which are like lists but have a statically-checked length. Here's an example function involving vectors: duplicate : (t : Type) -> t -> (n : Nat) -> (Vector n t) This type signature says that `duplicate` is a function of 3 arguments: `a -> b` means a function from argument type `a` to return type `b`, and `a -> b -> c` can either be interpreted as "a function taking an `a` and returning a `b -> c`" or (equivalently) "a function taking an `a` and a `b` and returning a `c` (see https://wiki.haskell.org/Currying https://wiki.haskell.org/Currying for why this is equivalent). Argument types are written in one of two ways: if they're written like `a` (for example `Int` or `String`), then the type of the argument is `a`; if they're written `a : b` (for example `age : Int`) then the argument type is `b`, but later types can refer to the value as `a`. So this signature says that the first argument of `duplicate` is called `t`, and it is a `Type`. The second argument has type `t`; this means the type of the second argument depends on the value of the first argument: if we call `duplicate` with `Bool : Type` as the first argument, then the second argument must be a `Bool`. The third argument is called `n`, and has type `Nat` (natural numbers: i.e. the positive integers including zero). The return type is `Vector n t`, i.e. a list of length `n` containing elements of type `t`. Note that we're referring to argument values by name, but we don't know what particular value they will be (i.e. which number `n` will be, or which type `t` will be). We can think of `a : b` as being `for all a of type b`. If we think about functions returning lists, like `map` or `reverse`, we can "cheat" by having them always return an empty list; such functions satisfy their type signature (they return a list), but don't behave in the way we want. In contrast, the "for all" nature of dependent function types can be used to prevent this sort of "cheating". The `duplicate` function can't just return an empty vector, since it must return a vector of length `n`, and the implementation must work for all values of `n`. We're forced to write a function which constructs a vector of the correct length: empty when `n` is zero, or non-empty otherwise. To construct a non-empty vector, we need to put a value inside it. What value can we use? We can't "cheat" by using, say, the value `"hello"`, since that would give us a vector containing `String`, whilst our return type forces us to make a vector containing `t`. Whatever our function does, it must work for all values of `t` (`String`, `Bool`, `Int`, `Vector 5 (Int -> Bool)`, etc.). Since we don't know what `t` will be, we can't "invent" a value of the right type. The only thing we can do is use an existing value which will always have type `t`. The only way something can have type `t` is if it appears in our type signature, since that's the scope of the name `t`. The only thing in our type signature which has type `t` is the second argument. Hence we must use the second argument as the elements of our vector (if it's non-empty). One implementation which satisfies this type is the following (assuming that `Nat` is encoded as Peano numerals https://en.wikipedia.org/wiki/Successor_function https://en.wikipedia.org/wiki/Successor_function ): duplicate t x n = case n of zero -> vectorNil t succ m -> vectorCons t x (duplicate t x m) This isn't the only possible implementation, for example we might choose to send the recursive call through a `vectorReverse` function (although it would be pointless), but such differences cannot alter the input/output behaviour of the function. Of course, we don't have to use dependent function types to restrict all of a function's behaviour. If we think back to the `map` example, we take a function of type `a -> b`, a `List a` and must return a `List b`: the easiest thing to do is return an empty list, which satisfies the type but isn't what we want. If we instead make a `vectorMap` function, where `List` is replaced with `Vector n`, then that "cheat" no longer works (since an empty vector doesn't always have length `n`). We could still mess around with the contents, like reversing it or doing some other permutation, but that's harder than just doing the right thing. The path of least resistance is to write a correct implementation!

fiddlerwoaroof 9y ago
I like the way Edwin Brady talks about this: a dependently typed language is one in which types are first class. That is, you can use them as values in computations and return them.
- chriswarbo 9y ago
  "First class types" and "dependent types" are actually two different things. We can have first class types without any dependencies. For example: isEven : Nat -> Type isEven zero = Unit isEven (succ zero) = Empty isEven (succ (succ n)) = isEven n fortyTwoEven : isEven 42 fortyTwoEven = unit Here the `isEven` function calculates a type based on the given number: if the number's even, it returns the `Unit` type, of which there is a value `unit`; if the number's odd, it returns the `Empty` type, of which there are no values. The value `fortyTwoEven` is a "proof" that the number `42` (which would actually be `succ (succ (succ ...))` nested 42 times) is even. The proof is the value `unit`, which will only work if `isEven 42` returns `Unit`, which will only happen if 42 is even, so everything works out. We can write a type like `isEven 43`, but that will return the type `Empty`, which there's no way to satisfy. We can use this sort of thing to do static checks of reasonably simple data; for example, if we have a bunch of config parameters which need to be related in some way. Dependent types add the "naming" part, which we can use in functions (as explained above), but also in other "compound" datastructures like tuples `(n : Nat, isEven n)` and records `{ n : Nat, evenProof : isEven n }` The annoying thing is that few languages seem to have first class types at all, so every explanation of dependent types has to start by introducing first class types, and then explaining the "dependent" parts. It's like trying to explain something like interfaces, if all mainstream languages were dynamically typed. We'd have to begin by explaining what types are, and then go on to explain interfaces. Readers might easily confuse features of types with features of interfaces, which would lead to much confusion. I think that's kind of happened with "dependent types" and "first class types", although I haven't seen any/many systems which have one without the other, so maybe it's not too bad :)
pmoriarty 9y ago
That was some of the clearest technical writing I've ever read. I hope you write a book, if you haven't already.