12 ms·

In Further Praise of Dependent Types

84 points by EvgeniyZh 6y ago

gitgud 6y ago
Is that the same as inheritance of types in CS?
- cjfd 6y ago
  No, it is not.
- mehrdadn 6y ago
  Nope, it's a Programming Language Theory thing. See here: https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type
- jmaa 6y ago
  No; lookup Calculus of Construction. Dependent types allows you to specify an dependence between different values in your type directly within your type system; which has great implications for type safety and so on. A classic example is that you can specify the 2-vectors on the unit circle as "{ (x,y) : x,y in R | x^2 + y^2 = 1 }" (read as "the set of real 2-tuples, where their norm is equal to 1".) This is not possible in most languages; the closest you can get in most languages is "{ (x,y) : x,y in R }". My personal pet peeve with dependent types and proof-driven programming in general is the wealth of options in formulating propositions. I've seen at least five different ways of defining equivalency.
  - fuoqi 6y ago
    >you can specify the 2-vectors on the unit circle as "{ (x,y) : x,y in R | x^2 + y^2 = 1 }" Which is not possible for any language targeting real machines since floats have fixed precision.
    - icen 6y ago
      You can specify the 2-vectors on the unit circle as "{ (x, y) : x, y in R | x^2 + y^2 - 1 < 0.000001 }" instead.
  - mehrdadn 6y ago
    To clarify, "great implications" can mean "undecidability".
- igravious 6y ago
  “a dependent type is a type whose definition depends on a value” So sayeth WikiP: https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type The example normally given is, for instance, being able to define a function whose return type depends of the value (not the type) of its argument – for example, a function which takes in a natural number and returns an array with exactly the length of that natural number. Dependent types are one of the axes in the Lambda Cube: https://en.wikipedia.org/wiki/Lambda_cube https://en.wikipedia.org/wiki/Lambda_cube – types have terms the way sets have elements (roughly speaking) and so you can [1] relate types with types (type operators), you can [2] relate terms with types (polymorphism), and lastly [3] types with terms (dependent types) – giving a three-dimensional type theoretic space. (Btw, I don't know if it even makes sense to talk about relating terms with terms or what feature of type theory captures this notion – so don't ask me!)
exdsq 6y ago
After playing with dependent types and type driven development, almost every language has been spoiled for me :(
- dgellow 6y ago
  Could you explain what was so great about it? I guess you did this with Idris?
  - icen 6y ago
    (Not OP.) When moving from dynamically/untyped/unityped languages to those with types, you are liberated from having to check the shape of inputs. If you're given something that claims to be a list of strings, it absolutely is a list of strings, and you can proceed without thinking about it's list-ness or string-ness any further. When moving from a typed language to a dependently typed language, you are liberated from having to check the state of inputs. You don't have to worry that your file handle is closed, or ensure that you update the state of the object correctly to satisfy some protocol (if you don't, you will be picked up on it!). If you are writing a parser, you don't need to check that the parser returned the form that you just called - you know upfront. There are other niceties: the type of the function is always a very rough exposition of what the function should do. With dependent types, it becomes considerably clearer. Consider these two functions, which could have very similar implementations (in some Idris-like syntax): f : Int -> Int -> Bool data T : Int -> Int -> Type where Tz : T 0 x Ts : T a b -> T (a + 1) (b + 1) g : (x : Int) -> (y : Int) -> Maybe (T x y) Given just the structure, it should be a bit clearer as to what's going the functions intend to do.
    - tsimionescu 6y ago
      But wouldn't the actual code tell you exactly what the function does? Why is it beneficial to have a similar version of the same in a more or less different language expressed separately? The flipside of your description of moving from un typed to typed to dependent typed languages is the amount of specification you need to think about and add to your code. This is awesome for component interfaces, but it can often get in the way of internal code. For example, if I try to redactor a long function and extract a few bits, those bits may only be called with very specific argument values, despite what the types I have on hand (or am willing to define) might say. Languages without some dynamic escape hatches can force you to create code that is too general, or define extremely specific types, for situations that really don't call for it. It also makes very generic or dynamic code much harder to write, or requiring ever more complex constructions. For example, most mainstream typed languages can't express something as simple as 'a function that returns either an A or a B' without resort g to dynamic typing and casting. And even in Haskell, a lot of code is more loosely typed than might be expected. For example, even though measurement units are often touted as a feature of typed languages, there are no complex mathematics libraries that use measurement units, simply because it is so much effort to correctly type everything, for relatively little gain.
curryhoward 6y ago
I've been meaning to write a tutorial on dependent types, but aimed at programmers rather than mathematicians and computer scientists. Here are some of the reasons I love them so much: - The most popular motivation: the ability to write proofs about your programs, using the same language for both programming and proving. It's so satisfying to write code and prove it correct (with a type checker to catch your mistakes), but so few people get to experience this feeling. - Of course, you can also use dependent types to just write proofs for the purpose of doing mathematics, without any programming. I've written about my experience doing that here: https://www.stephanboyer.com/post/134/my-hobby-proof-engineering https://www.stephanboyer.com/post/134/my-hobby-proof-enginee... - But dependent types are also useful in ordinary everyday programming! Many "features" of programming languages that we use at work are actually just limited special cases of the general idea of dependent types. For example, in a dependently typed language, you don't need special support for generics—you get it for free! - Dependent types also eliminate much of the need for macros. In Rust, for example, you might use a macro to generate a JSON parser for a given type. If you had dependent types, you could just write a function that takes your type as an argument and returns the parser! - Of course, there's that famous example of length-indexed vectors. The idea is that you can keep track of the sizes of your arrays in their types, and statically prevent out-of-bounds errors. So, for example, trying to get the first element of an empty array would be a type error. - Haskell's generalized algebraic datatypes are another example of a limited special case of the full power you'd get from a dependently typed programming language. - Another example: some languages have special support for existential types in some form or another. For example, Rust has something called "impl Trait" which is a limited use of existential types. This is another thing you get for free with dependent types (or rank-2 polymorphism). - Other examples of things you get for free with dependent types: type aliases, higher-kinded types, higher-rank types, and compile-time code execution. Dependent types may seem complicated at first glance. But after seeing how all these programming language features collapse into a single unified framework, you might change your mind: dependent types are extremely simple compared to the cornucopia of concepts we have to learn in their absence! I strongly believe that programming languages have grown too complex, and dependent types have the right power-to-weight ratio to cull that complexity.
- haneefmubarak 6y ago
nyanpasu64 6y ago
> So, a good place to try and understand underlying linguistic structure is informal mathematics, something he studied in his 1993 paper Type theory and the informal language of mathematics. This investigates both directions of the passage between formal and informal mathematics: sugaring and formalization. Okay... > x:A ⊢ B(x): Type I'm lost.
- icen 6y ago
  This is standard notation. The `x : A` supposes a value, `x`, inhabiting a type `A` (like in Rust, or ML, or maybe `A x` in C). On the right hand side of the turnstile, we have `B(x) : Type`, which is roughly what it looks like: `B` is a type parameterised by `x` (note - it is not parameterised by `A`, but by `x`! It is allowed to know about the value `x`). The central turnstile is a contextual relation. The left hand side is an ambient known value, and the right hand side is something that be defined in that context. You can read it informally as "given", so this phrase is "given x: A, we can construct a type B(x)".
- deleted 6y ago
  [deleted]
- curryhoward 6y ago
  Unfortunately you need to know type theory/logic notation in order to read this. Here's the English translation: - There is a variable called `x` in scope. - `x` is known to have type `A`. - `B` is a function that, when given `x` as an argument, returns a type. If this seems weird, it's because you need dependent types to even be able to say this. Honestly, this article is not written for programmers, and I don't know why it's on Hacker News right now. Most HN readers don't have the necessary background to follow it.
  - Gravityloss 6y ago
    Thank you, it is easy to understand when explained like that! Maybe there could be a programming language where these concepts were used but slightly more explicitly, verbosely or in general easier to read fashion. A lot of successful languages are big on ergonomics or low barriers for entry.
auggierose 6y ago
If you want to read a somewhat longer treatise about dependent types and language, try the book "Modal Homotopy Type Theory". Modal logic has been basically invented for linguistic problems. I don't think dependent types are essential for giving language a formal semantics though, I think discourse representation theory has a more direct approach.
benrbray 6y ago
> The main characteristic of the language of mathematics is perhaps that different members of the community can completely agree about the meaning of each word and sentence. Haha, this got a laugh out of me :). While this is true in principle, the reality can be quite messy! For instance, there seems to be little consensus about what the words "vector", "contravariant", "covariant", and "coordinate" should mean on the Wikipedia page [1] claiming to explain just that! [1] https://en.wikipedia.org/wiki/Talk:Covariance_and_contravariance_of_vectors https://en.wikipedia.org/wiki/Talk:Covariance_and_contravari...

84 points by EvgeniyZh 6y ago

gitgud 6y ago

Is that the same as inheritance of types in CS?

cjfd 6y ago
No, it is not.
mehrdadn 6y ago
Nope, it's a Programming Language Theory thing. See here: https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type
jmaa 6y ago
No; lookup Calculus of Construction. Dependent types allows you to specify an dependence between different values in your type directly within your type system; which has great implications for type safety and so on. A classic example is that you can specify the 2-vectors on the unit circle as "{ (x,y) : x,y in R | x^2 + y^2 = 1 }" (read as "the set of real 2-tuples, where their norm is equal to 1".) This is not possible in most languages; the closest you can get in most languages is "{ (x,y) : x,y in R }". My personal pet peeve with dependent types and proof-driven programming in general is the wealth of options in formulating propositions. I've seen at least five different ways of defining equivalency.
- fuoqi 6y ago
  >you can specify the 2-vectors on the unit circle as "{ (x,y) : x,y in R | x^2 + y^2 = 1 }" Which is not possible for any language targeting real machines since floats have fixed precision.
  - icen 6y ago
    You can specify the 2-vectors on the unit circle as "{ (x, y) : x, y in R | x^2 + y^2 - 1 < 0.000001 }" instead.
- mehrdadn 6y ago
  To clarify, "great implications" can mean "undecidability".
igravious 6y ago
“a dependent type is a type whose definition depends on a value” So sayeth WikiP: https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type The example normally given is, for instance, being able to define a function whose return type depends of the value (not the type) of its argument – for example, a function which takes in a natural number and returns an array with exactly the length of that natural number. Dependent types are one of the axes in the Lambda Cube: https://en.wikipedia.org/wiki/Lambda_cube https://en.wikipedia.org/wiki/Lambda_cube – types have terms the way sets have elements (roughly speaking) and so you can [1] relate types with types (type operators), you can [2] relate terms with types (polymorphism), and lastly [3] types with terms (dependent types) – giving a three-dimensional type theoretic space. (Btw, I don't know if it even makes sense to talk about relating terms with terms or what feature of type theory captures this notion – so don't ask me!)

exdsq 6y ago

After playing with dependent types and type driven development, almost every language has been spoiled for me :(

dgellow 6y ago
Could you explain what was so great about it? I guess you did this with Idris?
- icen 6y ago
  (Not OP.) When moving from dynamically/untyped/unityped languages to those with types, you are liberated from having to check the shape of inputs. If you're given something that claims to be a list of strings, it absolutely is a list of strings, and you can proceed without thinking about it's list-ness or string-ness any further. When moving from a typed language to a dependently typed language, you are liberated from having to check the state of inputs. You don't have to worry that your file handle is closed, or ensure that you update the state of the object correctly to satisfy some protocol (if you don't, you will be picked up on it!). If you are writing a parser, you don't need to check that the parser returned the form that you just called - you know upfront. There are other niceties: the type of the function is always a very rough exposition of what the function should do. With dependent types, it becomes considerably clearer. Consider these two functions, which could have very similar implementations (in some Idris-like syntax): f : Int -> Int -> Bool data T : Int -> Int -> Type where Tz : T 0 x Ts : T a b -> T (a + 1) (b + 1) g : (x : Int) -> (y : Int) -> Maybe (T x y) Given just the structure, it should be a bit clearer as to what's going the functions intend to do.
  - tsimionescu 6y ago
    But wouldn't the actual code tell you exactly what the function does? Why is it beneficial to have a similar version of the same in a more or less different language expressed separately? The flipside of your description of moving from un typed to typed to dependent typed languages is the amount of specification you need to think about and add to your code. This is awesome for component interfaces, but it can often get in the way of internal code. For example, if I try to redactor a long function and extract a few bits, those bits may only be called with very specific argument values, despite what the types I have on hand (or am willing to define) might say. Languages without some dynamic escape hatches can force you to create code that is too general, or define extremely specific types, for situations that really don't call for it. It also makes very generic or dynamic code much harder to write, or requiring ever more complex constructions. For example, most mainstream typed languages can't express something as simple as 'a function that returns either an A or a B' without resort g to dynamic typing and casting. And even in Haskell, a lot of code is more loosely typed than might be expected. For example, even though measurement units are often touted as a feature of typed languages, there are no complex mathematics libraries that use measurement units, simply because it is so much effort to correctly type everything, for relatively little gain.

curryhoward 6y ago

I've been meaning to write a tutorial on dependent types, but aimed at programmers rather than mathematicians and computer scientists. Here are some of the reasons I love them so much: - The most popular motivation: the ability to write proofs about your programs, using the same language for both programming and proving. It's so satisfying to write code and prove it correct (with a type checker to catch your mistakes), but so few people get to experience this feeling. - Of course, you can also use dependent types to just write proofs for the purpose of doing mathematics, without any programming. I've written about my experience doing that here: https://www.stephanboyer.com/post/134/my-hobby-proof-engineering https://www.stephanboyer.com/post/134/my-hobby-proof-enginee... - But dependent types are also useful in ordinary everyday programming! Many "features" of programming languages that we use at work are actually just limited special cases of the general idea of dependent types. For example, in a dependently typed language, you don't need special support for generics—you get it for free! - Dependent types also eliminate much of the need for macros. In Rust, for example, you might use a macro to generate a JSON parser for a given type. If you had dependent types, you could just write a function that takes your type as an argument and returns the parser! - Of course, there's that famous example of length-indexed vectors. The idea is that you can keep track of the sizes of your arrays in their types, and statically prevent out-of-bounds errors. So, for example, trying to get the first element of an empty array would be a type error. - Haskell's generalized algebraic datatypes are another example of a limited special case of the full power you'd get from a dependently typed programming language. - Another example: some languages have special support for existential types in some form or another. For example, Rust has something called "impl Trait" which is a limited use of existential types. This is another thing you get for free with dependent types (or rank-2 polymorphism). - Other examples of things you get for free with dependent types: type aliases, higher-kinded types, higher-rank types, and compile-time code execution. Dependent types may seem complicated at first glance. But after seeing how all these programming language features collapse into a single unified framework, you might change your mind: dependent types are extremely simple compared to the cornucopia of concepts we have to learn in their absence! I strongly believe that programming languages have grown too complex, and dependent types have the right power-to-weight ratio to cull that complexity.

haneefmubarak 6y ago

nyanpasu64 6y ago

> So, a good place to try and understand underlying linguistic structure is informal mathematics, something he studied in his 1993 paper Type theory and the informal language of mathematics. This investigates both directions of the passage between formal and informal mathematics: sugaring and formalization. Okay... > x:A ⊢ B(x): Type I'm lost.

icen 6y ago
This is standard notation. The `x : A` supposes a value, `x`, inhabiting a type `A` (like in Rust, or ML, or maybe `A x` in C). On the right hand side of the turnstile, we have `B(x) : Type`, which is roughly what it looks like: `B` is a type parameterised by `x` (note - it is not parameterised by `A`, but by `x`! It is allowed to know about the value `x`). The central turnstile is a contextual relation. The left hand side is an ambient known value, and the right hand side is something that be defined in that context. You can read it informally as "given", so this phrase is "given x: A, we can construct a type B(x)".
deleted 6y ago
[deleted]
curryhoward 6y ago
Unfortunately you need to know type theory/logic notation in order to read this. Here's the English translation: - There is a variable called `x` in scope. - `x` is known to have type `A`. - `B` is a function that, when given `x` as an argument, returns a type. If this seems weird, it's because you need dependent types to even be able to say this. Honestly, this article is not written for programmers, and I don't know why it's on Hacker News right now. Most HN readers don't have the necessary background to follow it.
- Gravityloss 6y ago
  Thank you, it is easy to understand when explained like that! Maybe there could be a programming language where these concepts were used but slightly more explicitly, verbosely or in general easier to read fashion. A lot of successful languages are big on ergonomics or low barriers for entry.

auggierose 6y ago

If you want to read a somewhat longer treatise about dependent types and language, try the book "Modal Homotopy Type Theory". Modal logic has been basically invented for linguistic problems. I don't think dependent types are essential for giving language a formal semantics though, I think discourse representation theory has a more direct approach.

benrbray 6y ago

> The main characteristic of the language of mathematics is perhaps that different members of the community can completely agree about the meaning of each word and sentence. Haha, this got a laugh out of me :). While this is true in principle, the reality can be quite messy! For instance, there seems to be little consensus about what the words "vector", "contravariant", "covariant", and "coordinate" should mean on the Wikipedia page [1] claiming to explain just that! [1] https://en.wikipedia.org/wiki/Talk:Covariance_and_contravariance_of_vectors https://en.wikipedia.org/wiki/Talk:Covariance_and_contravari...