4 ms·

Does anybody care to explain dependent types? I’ve heard the term used in FP conversations but not sure I get it.

huntie 8y ago
Dependent types are types which depend on values. As an example, think of the cons procedure: (List A, A) -> List A. It takes a List of A's and an A and returns a List of A's. With dependent types you can write this as (List n A, A) -> List n+1 A. This tells us that cons takes a List of A's with length n and an A returns a List of A's with length n+1. Edwin Brady shows off some examples in Idris here[1]. I thought the matrix example was really impressive. [1] https://www.youtube.com/watch?v=mOtKD7ml0NU https://www.youtube.com/watch?v=mOtKD7ml0NU
- joe_the_user 8y ago
  When I see this definition, I scratch my head and wonder why this isn't a different way to introduce object orientation, generics, c++ parameterized templates and such.
  - RossBencina 8y ago
    Yes. C++ templates provide some subset of what you can do with dependent types in Idris.
  - logicchains 8y ago
    The key difference with C++ templates is that in C++ you can't have a type parameterised by a value that's only know at runtime, e.g. a std::array<N> where N is read from stdin. In a dependently typed language, you can. Object orientation is a different matter entirely; in the sense it implies Java-style class-based inheritance, it's almost in the opposite spirit to dependent types, as such late-binding (virtual methods) means it's possible to call methods such that the compiler has no idea which method will be called at compile time, making it hard to reason about the code at compile time.
    - deleted 8y ago
      [deleted]
  - deleted 8y ago
    [deleted]
pjmlp 8y ago
In a very abstract way, it is a way to encode relationships between types on the type system. You can express things like how are you allowed to consume elements from a data structure, how many elements a specific data structure is allowed/expected to have, how their form looks like and so forth, all at compile time. Thus working as kind of profs that certain functions can only be called if the conditions are met. https://en.wikipedia.org/wiki/Type_system https://en.wikipedia.org/wiki/Type_system
hiker 8y ago
Most typed languages have two separate levels: expressions (and statements in imperative languages) and types. Dependent types unify those two levels into one. This allows one to use values in types, or vice versa, effectively making types first class in the sense that functional programming makes functions first class. As an example this is Haskell's core language: data Expr b = Var Id | Lit Literal | App (Expr b) (Arg b) | Lam b (Expr b) | Let (Bind b) (Expr b) | Case (Expr b) b Type [Alt b] | Tick (Tickish Id) (Expr b) | Type Type | Cast (Expr b) Coercion | Coercion Coercion data Type = TyVarTy Var | LitTy TyLit | AppTy Type Type | ForAllTy !TyCoVarBinder Type | FunTy Type Type | TyConApp TyCon [KindOrType] | CastTy Type KindCoercion | CoercionTy Coercion If you look closely you'll notice quite a lot of duplication between the two (see the first 4 and the last 2 constructors). Haskell is effectevily using the same language (lambda calculus) to describe types and expressions though with different syntax. And this is Lean core language (a dependently type language): inductive expr | var : nat → expr | sort : level → expr | const : name → list level → expr | mvar : name → name → expr → expr | local_const : name → name → binder_info → expr → expr | app : expr → expr → expr | lam : name → binder_info → expr → expr → expr | pi : name → binder_info → expr → expr → expr | elet : name → expr → expr → expr → expr | macro : macro_def → list expr → expr Imo dependent types provide a surprising answer to the question "What is the best type system?". Different languages have different type systems and as they evolve to become more expressive at a certain point they become Turing complete (e.g. C++, Typescript, Haskell, ..). So we end up with two separate languages - the language itself to describe programs and the type system to describe types. So what's the best type system? Dependent types' answer: the language itself. Instead of having two separate languages, have a single language that acts as its own type system, powerful enough to describe both programs and types. Then types become first class - you can pass them to a function as parameters, or return them as values, or use any function at compile time. In physics progress usually comes in the form of unification. Two seemingly separate phenomena (say electricity and magnetism) turn out to be described by a single theory. Dependent types provide such a unification between expressions and types in programming languages. Imo definitely a step forward in the noisy sea of programming languages. That's not even touching the mathematical side of things, Curry-Howard correspondence, proof assistants and using dependent types for proving theorems.
tpush 8y ago
When the type of a function mentions its parameter, it’s a dependent type (just like a normal function that mentions it’s parameter is a “dependent value”, so to speak. Usually though one speaks of dependent types only when the parameter can range over not just types.
topmonk 8y ago
Imagine that you take a type from C or Java or something and add the ability to convert it into another type. I'm not talking about casting an int to a float, but actually manipulating the type without doing anything on the data side. Now allow arbitrary programs to be types. We'll call these type programs. Now imagine a game where you take one type program and try to convert it into another while proving to the compiler that it still does the same thing. For example, say you had a function foo (int x) { return x+1; }, and the type program A “foo(a+1)”, and the type program B “foo(foo(a))”. Your job would be to change A to look exactly like B, or vice versa, using commands built into the language itself. Why would you want to do this? Because it's been shown using a certain type of mathematics, called constructive mathematics, you can create type programs to represent any hypothesis you would like: m + n = n + m, for example. Then you can use the built in commands to change a type into another type to represent a proof of the hypothesis. In this way you can prove hypotheses related to your program, (or anything really) as long as you construct the right types and use the built in commands to change prove the hypotheses true. You really need to learn a lot of things to understand how this translation from types to proofs work, so I didn't try to explain that here. I find the whole thing fascinating myself, but haven't gone too deeply into it. (BTW, if anyone more knowledgeable sees something I've written that is wrong here, please correct me, for my own information more than anything else)
joppy 8y ago
Most typed programming languages will allow you to form a pair of type (Integer, Integer), and reject programs which try to return something like (Integer, Float). Dependently typed languages might allow you to declare a type (n, m) where n and m are integers, and n < m, and will reject programs which attempt to return pairs with n > m. The key step here is that this rejection is done during compilation, and so while your program is running you can be absolutely sure that n < m.
mietek 8y ago
Two sentence summary that glosses over a lot of things: 1. Types can be used to classify programs. 2. Dependent types can be used to classify programs by running other programs on them. If you would like to learn more about dependent types, ‘The Little Typer’ is newly out and a lot of fun to read: https://mitpress.mit.edu/books/little-typer https://mitpress.mit.edu/books/little-typer

Dependent types are types which depend on values. As an example, think of the cons procedure: (List A, A) -> List A. It takes a List of A's and an A and returns a List of A's. With dependent types you can write this as (List n A, A) -> List n+1 A. This tells us that cons takes a List of A's with length n and an A returns a List of A's with length n+1. Edwin Brady shows off some examples in Idris here[1]. I thought the matrix example was really impressive. [1] https://www.youtube.com/watch?v=mOtKD7ml0NU https://www.youtube.com/watch?v=mOtKD7ml0NU

joe_the_user 8y ago
When I see this definition, I scratch my head and wonder why this isn't a different way to introduce object orientation, generics, c++ parameterized templates and such.
- RossBencina 8y ago
  Yes. C++ templates provide some subset of what you can do with dependent types in Idris.
- logicchains 8y ago
  The key difference with C++ templates is that in C++ you can't have a type parameterised by a value that's only know at runtime, e.g. a std::array<N> where N is read from stdin. In a dependently typed language, you can. Object orientation is a different matter entirely; in the sense it implies Java-style class-based inheritance, it's almost in the opposite spirit to dependent types, as such late-binding (virtual methods) means it's possible to call methods such that the compiler has no idea which method will be called at compile time, making it hard to reason about the code at compile time.
  - deleted 8y ago
    [deleted]
- deleted 8y ago
  [deleted]

pjmlp 8y ago

In a very abstract way, it is a way to encode relationships between types on the type system. You can express things like how are you allowed to consume elements from a data structure, how many elements a specific data structure is allowed/expected to have, how their form looks like and so forth, all at compile time. Thus working as kind of profs that certain functions can only be called if the conditions are met. https://en.wikipedia.org/wiki/Type_system https://en.wikipedia.org/wiki/Type_system

hiker 8y ago

Most typed languages have two separate levels: expressions (and statements in imperative languages) and types. Dependent types unify those two levels into one. This allows one to use values in types, or vice versa, effectively making types first class in the sense that functional programming makes functions first class. As an example this is Haskell's core language: data Expr b = Var Id | Lit Literal | App (Expr b) (Arg b) | Lam b (Expr b) | Let (Bind b) (Expr b) | Case (Expr b) b Type [Alt b] | Tick (Tickish Id) (Expr b) | Type Type | Cast (Expr b) Coercion | Coercion Coercion data Type = TyVarTy Var | LitTy TyLit | AppTy Type Type | ForAllTy !TyCoVarBinder Type | FunTy Type Type | TyConApp TyCon [KindOrType] | CastTy Type KindCoercion | CoercionTy Coercion If you look closely you'll notice quite a lot of duplication between the two (see the first 4 and the last 2 constructors). Haskell is effectevily using the same language (lambda calculus) to describe types and expressions though with different syntax. And this is Lean core language (a dependently type language): inductive expr | var : nat → expr | sort : level → expr | const : name → list level → expr | mvar : name → name → expr → expr | local_const : name → name → binder_info → expr → expr | app : expr → expr → expr | lam : name → binder_info → expr → expr → expr | pi : name → binder_info → expr → expr → expr | elet : name → expr → expr → expr → expr | macro : macro_def → list expr → expr Imo dependent types provide a surprising answer to the question "What is the best type system?". Different languages have different type systems and as they evolve to become more expressive at a certain point they become Turing complete (e.g. C++, Typescript, Haskell, ..). So we end up with two separate languages - the language itself to describe programs and the type system to describe types. So what's the best type system? Dependent types' answer: the language itself. Instead of having two separate languages, have a single language that acts as its own type system, powerful enough to describe both programs and types. Then types become first class - you can pass them to a function as parameters, or return them as values, or use any function at compile time. In physics progress usually comes in the form of unification. Two seemingly separate phenomena (say electricity and magnetism) turn out to be described by a single theory. Dependent types provide such a unification between expressions and types in programming languages. Imo definitely a step forward in the noisy sea of programming languages. That's not even touching the mathematical side of things, Curry-Howard correspondence, proof assistants and using dependent types for proving theorems.

tpush 8y ago

When the type of a function mentions its parameter, it’s a dependent type (just like a normal function that mentions it’s parameter is a “dependent value”, so to speak. Usually though one speaks of dependent types only when the parameter can range over not just types.

topmonk 8y ago

Imagine that you take a type from C or Java or something and add the ability to convert it into another type. I'm not talking about casting an int to a float, but actually manipulating the type without doing anything on the data side. Now allow arbitrary programs to be types. We'll call these type programs. Now imagine a game where you take one type program and try to convert it into another while proving to the compiler that it still does the same thing. For example, say you had a function foo (int x) { return x+1; }, and the type program A “foo(a+1)”, and the type program B “foo(foo(a))”. Your job would be to change A to look exactly like B, or vice versa, using commands built into the language itself. Why would you want to do this? Because it's been shown using a certain type of mathematics, called constructive mathematics, you can create type programs to represent any hypothesis you would like: m + n = n + m, for example. Then you can use the built in commands to change a type into another type to represent a proof of the hypothesis. In this way you can prove hypotheses related to your program, (or anything really) as long as you construct the right types and use the built in commands to change prove the hypotheses true. You really need to learn a lot of things to understand how this translation from types to proofs work, so I didn't try to explain that here. I find the whole thing fascinating myself, but haven't gone too deeply into it. (BTW, if anyone more knowledgeable sees something I've written that is wrong here, please correct me, for my own information more than anything else)

joppy 8y ago

Most typed programming languages will allow you to form a pair of type (Integer, Integer), and reject programs which try to return something like (Integer, Float). Dependently typed languages might allow you to declare a type (n, m) where n and m are integers, and n < m, and will reject programs which attempt to return pairs with n > m. The key step here is that this rejection is done during compilation, and so while your program is running you can be absolutely sure that n < m.

mietek 8y ago

Two sentence summary that glosses over a lot of things: 1. Types can be used to classify programs. 2. Dependent types can be used to classify programs by running other programs on them. If you would like to learn more about dependent types, ‘The Little Typer’ is newly out and a lot of fun to read: https://mitpress.mit.edu/books/little-typer https://mitpress.mit.edu/books/little-typer