4 ms·

Could someone clarify to me the different between dependent types and refinement types?

dietr1ch 2y ago
Refinements embed a predicate that elements of the new type must pass. def Nat = Int: (|x| -> x >= 0) Dependent types allow types to be computed from functions (and depend on arguments, otherwise it seems they become just weird constants), def Five(as_type: String) -> NumericType(as_type): match as_type: "string" => "five" "int" => 5 "float" => 5.0f "double" => 5.0d _ => panic() // Unnecessary if you refine `as_type` from a String to an enum or a fixed set of strings. Dependent types seem weird, but they help making types first-class (https://www.youtube.com/watch?v=mOtKD7ml0NU&t=325s https://www.youtube.com/watch?v=mOtKD7ml0NU&t=325s) and gaining types like `Array<T, N>` that allow ensuring things are the right length, and define append/extend properly.
- xigoi 2y ago
  Just curious, what language is this?
  - dietr1ch 2y ago
    I made up the syntax to try to keep it easy to read for people using python/rust/c. I just realized my lambda syntax on the Nat predicate is redundant because I didn't clean up and that using snake_case for function names would be better in a language that lets you operate on functions like they are values.
- tubthumper8 2y ago
  What happens when the predicate returns false for the refinement type? Like if `(Nat 5) - (Nat 6)`. Or is subtraction disallowed?
  - klibertp 2y ago
    My understanding is that you get a type error when the type checker cannot prove the result of an operation conforms to a refined type. For constants, it's easy: `(Nat 5) - (Nat 3)` is Nat while `(Nat 5) - (Nat 6)` is a type error. For values coming from elsewhere, you need to give the type-checker some guarantee yourself: let x = Nat 5; let y = read_nat(); assert y < x; // without this, the following would fail to type check x - y (you need occurrence typing, too, in this example) In terms of numbers, what you can expect from refinement types is similar to what you get with CLP(FD) in Prolog.
    - tubthumper8 2y ago
      Right, but what happens if the Assert isn't true? Does the program crash/abort? If so, is there a stack trace or how do you troubleshoot it?
      - klibertp 2y ago
        It's a standard assert, so whatever happens on assertion failure normally happens here, too. This is orthogonal to refinement types - they are concerned with whether the check is made or not (ie. with them you cannot accidentally forget to write that assert). The check failing is a runtime concern (similar to dynamic cast failure), the type system has nothing to do with that.
      - dietr1ch 2y ago
        I guess the only natural way would be to have operations send you back to the Base type, and then have a `TryInto(v: Base) -> Result<Refined>` function that would verify the predicate and allow you getting back into the refined type. Maybe some operations can be proved to stay within the refined type, like adding natural numbers, but that's something that the used would need to provide as a function allowing that under assertions or some proof that the compiler can verify and trust.
demurgos 2y ago
Dependent types can make type constructors generic over _values_ (instead of only types). Refinement types keep the separation between types and values, but they let you wrap an existing type to enforce extra constraints or semantics. Another example of refinement are pattern types where you can attach a match pattern that is enforced to pass.
burakemir 2y ago
Dependent types typically refers to type systems where a type can depend on a term. The canonical example is "Vector n" where n is some expression that evaluates to a natural number. Refinement types typically(1) refers to a type systems that lets you create a subtype of a type through refining (qualifying) with a predicate or constraint on the shape. Examples {x \in int | is_even x } or { x \in List | len(x) = 1 } Refinement types can be very powerful but that may well make type checking undecidable (think of a type of Turing machines, and the refinement that keeps only the ones that halt). By being careful about the logic used in the refinements, one may retain decidability. (1) The article seems to have a different idea of what a refinement type is: quote "a type system that does its work after another type system has already done its work". I am not going to play orthodox guardian of type theory terminology here, yet to me personally, it does seem unfortunate to use that term. The author seems to really want a form of type-level computation, which could be interesting if it could be rigorously specified and it's relation to the existing type level reduction clarified.
akdor1154 2y ago
You could just read the first paragraph of TFA?

Refinements embed a predicate that elements of the new type must pass. def Nat = Int: (|x| -> x >= 0) Dependent types allow types to be computed from functions (and depend on arguments, otherwise it seems they become just weird constants), def Five(as_type: String) -> NumericType(as_type): match as_type: "string" => "five" "int" => 5 "float" => 5.0f "double" => 5.0d _ => panic() // Unnecessary if you refine `as_type` from a String to an enum or a fixed set of strings. Dependent types seem weird, but they help making types first-class (https://www.youtube.com/watch?v=mOtKD7ml0NU&t=325s https://www.youtube.com/watch?v=mOtKD7ml0NU&t=325s) and gaining types like `Array<T, N>` that allow ensuring things are the right length, and define append/extend properly.

xigoi 2y ago
Just curious, what language is this?
- dietr1ch 2y ago
  I made up the syntax to try to keep it easy to read for people using python/rust/c. I just realized my lambda syntax on the Nat predicate is redundant because I didn't clean up and that using snake_case for function names would be better in a language that lets you operate on functions like they are values.
tubthumper8 2y ago
What happens when the predicate returns false for the refinement type? Like if `(Nat 5) - (Nat 6)`. Or is subtraction disallowed?
- klibertp 2y ago
  My understanding is that you get a type error when the type checker cannot prove the result of an operation conforms to a refined type. For constants, it's easy: `(Nat 5) - (Nat 3)` is Nat while `(Nat 5) - (Nat 6)` is a type error. For values coming from elsewhere, you need to give the type-checker some guarantee yourself: let x = Nat 5; let y = read_nat(); assert y < x; // without this, the following would fail to type check x - y (you need occurrence typing, too, in this example) In terms of numbers, what you can expect from refinement types is similar to what you get with CLP(FD) in Prolog.
  - tubthumper8 2y ago
    Right, but what happens if the Assert isn't true? Does the program crash/abort? If so, is there a stack trace or how do you troubleshoot it?
    - klibertp 2y ago
      It's a standard assert, so whatever happens on assertion failure normally happens here, too. This is orthogonal to refinement types - they are concerned with whether the check is made or not (ie. with them you cannot accidentally forget to write that assert). The check failing is a runtime concern (similar to dynamic cast failure), the type system has nothing to do with that.
    - dietr1ch 2y ago
      I guess the only natural way would be to have operations send you back to the Base type, and then have a `TryInto(v: Base) -> Result<Refined>` function that would verify the predicate and allow you getting back into the refined type. Maybe some operations can be proved to stay within the refined type, like adding natural numbers, but that's something that the used would need to provide as a function allowing that under assertions or some proof that the compiler can verify and trust.

demurgos 2y ago

Dependent types can make type constructors generic over _values_ (instead of only types). Refinement types keep the separation between types and values, but they let you wrap an existing type to enforce extra constraints or semantics. Another example of refinement are pattern types where you can attach a match pattern that is enforced to pass.

burakemir 2y ago

Dependent types typically refers to type systems where a type can depend on a term. The canonical example is "Vector n" where n is some expression that evaluates to a natural number. Refinement types typically(1) refers to a type systems that lets you create a subtype of a type through refining (qualifying) with a predicate or constraint on the shape. Examples {x \in int | is_even x } or { x \in List | len(x) = 1 } Refinement types can be very powerful but that may well make type checking undecidable (think of a type of Turing machines, and the refinement that keeps only the ones that halt). By being careful about the logic used in the refinements, one may retain decidability. (1) The article seems to have a different idea of what a refinement type is: quote "a type system that does its work after another type system has already done its work". I am not going to play orthodox guardian of type theory terminology here, yet to me personally, it does seem unfortunate to use that term. The author seems to really want a form of type-level computation, which could be interesting if it could be rigorously specified and it's relation to the existing type level reduction clarified.

akdor1154 2y ago

You could just read the first paragraph of TFA?