3 ms·

Is that the same as inheritance of types in CS?

by gitgud 6y ago

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!)

Is that the same as inheritance of types in CS?

by 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!)