8 ms·

Dependent Types for F#

136 points by jackfoxy 9y ago

rob-kuz 9y ago
Very cool library that Jack implemented here using an idea from my blog. We are using it in production. Works really nice.
- deleted 9y ago
  [deleted]
xyz-x 9y ago
Nice lib and library tests!
lkitching 9y ago
Does this library actually allow you to express dependent types or is it just for runtime validation? I can't see any examples in the documentation of a type depending on a value like the common let v : Vect 3 Int = [1,2,3] example. There aren't many types shown in the examples but it looks like let myNonEmptyIntSetOpt = [] |> Set.ofList |> NonEmptyIntSet.TryCreate would just return None at runtime rather than a compilation error?
- jackfoxy 9y ago
  How can you do a compile time check on data that has not entered the system? You can apply the same technique to Vect 3 [1,2,3] or any other type.
  - jackfoxy 9y ago
    a dependent type is a type whose definition depends on a value https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type
  - lkitching 9y ago
    How do you express the type `Vect 3 Int` using this library? F# doesn't support it and all the example types appear to depend on other types, not on values like 3.
    - jackfoxy 9y ago
      I'm pretty sure there are vector libraries available to F#. Dig around and you will find them. Then just apply dependent type to a type in that library. I don't work with them myself.
      - lkitching 9y ago
        I'm not asking specifically about vectors, that's just a common example of a dependent type. To take another example from the documentation, can you express a type like type digits = RegexString (Regex "^[0-9]+$") where all values of type digits are strings containing only digits? Then let s1 : digits = "1234" would typecheck but let s2 : digits = "abc" would not? That would be very surprising given the F# type system.
    - vorotato 9y ago
      Basically when you take some value the user gives you and cast it to the dependent type, you can then cover the case where you got some result because the cast was successful or you got none. You can't have dependent types at compile time, at least not completely so, though you could use something like fslint to catch any data being entered in code. https://news.ycombinator.com/item?id=7567310 https://news.ycombinator.com/item?id=7567310
      - vorotato 9y ago
        it would seem that in practice you can go even further, essentially writing exhaustive proofs. However F* already supports this and compiles to F#, so I would say if you want that level of correctness you should probably use a language which is better at describing the totality of a function.
  - deleted 9y ago
    [deleted]
  - cstrahan 9y ago
    > How can you do a compile time check on data that has not entered the system? You would have to supply proof that your types are correct; when you have a value who's type you'll only know at run time, you'll need to perform case analysis to bring additional info about the value's type into scope in the respective branches. To make concrete what I'm describing here, I'll use Idris's ++ (concatenation) as an example, which provides an inductive proof for the length of the resulting vector: (++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem (++) [] ys = ys (++) (x::xs) ys = x :: xs ++ ys The first line is the type signature, which claims that the length of the resulting vector is the sum of the lengths of the two argument vectors. The second line pattern matches on the null/empty constructor of the vector, and then returns ys. By pattern matching on the null constructor, we know that m == 0. We also know that n == length ys (whatever that may be). We know that 0 + x = x, so if we apply that to this case, we know that: length ([] ++ ys) == length [] + length ys == 0 + length ys == length ys == n == m + n (because we know m==0, and 0+n==n) ... so the compiler is happy here. The third and final line pattern matches on the non-empty (or cons, if you're a fan of Lisp) constructor. If this pattern applies, then we can make use of the fact that length (x::xs) == 1 + length xs. Of course, that that implies length xs < length (x::xs). That permits us to apply our induction hypothesis to the (xs ++ ys) sub expression, which tells that length (xs ++ ys) == length xs + length ys. Putting all of that together, we see that length (x :: xs ++ ys) == 1 + length (xs ++ ys) == 1 + length xs + length ys == 1 + (m - 1) + length ys == m + length ys == m + n That concludes our proof by induction[1]. Note that this proof is checked completely at compile time, and that it is still valid in the face of types which we won't know until we run our program. That's what dependent types give you. Here's an example that would not compile: (++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem (++) [] ys = ys (++) (x::xs) ys = x :: x :: xs ++ ys {- !!! note that I cons x here *twice* -} In conclusion, your library sounds like it could be an excellent way to provide smart constructors; at the same time, it's important to not conflate smart constructors with dependent types. I would urge you to continue developing your library, though I would recommend switching the name to something that's more indicative of what it actually does. That would have the additional benefit of not confusing people who read your project description and are hearing about dependent types for the first time. [1]: https://en.wikipedia.org/wiki/Mathematical_induction https://en.wikipedia.org/wiki/Mathematical_induction
Animats 9y ago
It's like subclassing, but it has to be called something else to be cool. Objects are so last-cen.
- joeblubaugh 9y ago
  It's significantly different than subclassing. The wikipedia examples are instructive: a dependent type is a type whose definition depends on a value. A "pair of integers" is a type. A "pair of integers where the second is greater than the first" is a dependent type because of the dependence on the value.
  - Animats 9y ago
    That's a subclass with an object invariant. (Gotta use the new buzzwords to be l33t. Even for old ideas.)
    - joeblubaugh 9y ago
      Sure, so if you use Ada you can write types like this and the runtime will enforce your invariants automatically. What other non-academic languages support that? It’s something I miss from Ada for sure.
- dwohnitmok 9y ago
  You're right in that what's being demonstrated here should actually be old-hat for OO programmers. It's basically a factory that returns things wrapped in an option if pre-conditions fail. Crucially what's being demonstrated here isn't dependent types at least as they are commonly known (which some of the comments here explain). Dependent types are when expressions can not only be of a type, but can also return a type. That means for example something like x : (if condition then Boolean else Int) is a type, i.e. the entire thing within the parentheses to the right of the y. This is radically different from subclassing. That entire if statement is a type, not just the `Boolean` or `Int` parts. Indeed because now arbitrary expressions (in particular equality can return a type!) can return types, types can be statements of your program and simply getting the typechecker to accept the type proves properties of your program. x : 5 = 5 In here "5 = 5" is a type. This flips normal statically typed programming on its head. We care more about the type than the value! The actual value of "x" is probably not something you care about; it just proves (in this case the trivial statement) that "5 = 5." Less trivial equalities can be stated additionCommutes : (a : Int, b : Int) -> a + b = b + a and proved by providing a value for additionCommutes that satisfies the typechecker. Again the important thing is the entire right-hand-side of additionCommutes is a single type.
phillipcarter 9y ago
This looks neat!
HumanDrivenDev 9y ago
Is there a reason dependent types aren't more widely used? Is it just a case of people not wanting to learn anything new, or are there some show-stopping issues in practice? The idea seems promising. If I'm not mistaken it would let you statically declare that an integer had to be between values X and Y, for example.
- skybrian 9y ago
  Lack of compelling tutorials for beginners? The examples I've seen are either solving toy problems in a complicated way or not understandable at all.
  - HumanDrivenDev 9y ago
    What's a toy problem in this case? Anything where you can replace even part of a dynamic contract seems like a win.
    - platz 9y ago
      > twblalock 468 days ago [-] > The Idris example seems to need further explanation: >> In Idris, we can say "the add function takes two integers and returns an integer, but its first argument must be smaller than its second argument": >> add : (x : Nat) -> (y : Nat) -> {auto smaller : LT x y} -> Nat >> add x y = x + y >That's all well and good, if you know the values of x and y at compile time. Consider a program that reads x and y from STDIN. The user could provide an x that is equal to or larger than y (or could provide only one value, or values that are not numbers). I see no way to deal with that except to throw a runtime error. Is that what would happen? In the case where the values are read from the external environment, first you would have to compare them before calling the function. The comparator would return either a proof that x <= y, or x > y. the proof ensures that at compile time you cannot mess this up. in other words, You have to perform the check at runtime, but the results for the check are enforced via a proof that is ensured to be correct at compile time. Connecting the proof the to the type system at compile time is the magic of dependent types > 18 points by platz 468 days ago [-] here's a full code example in Idris: import Data.String -- takes two integers, and a proof that x < y, and yields an integer add : (x : Integer) -> (y : Integer) -> (prf : x < y = True) -> -- require a proof that that x < y Integer add x y prf = x + y main : IO () main = do sx <- getLine -- read string from input sy <- getLine -- read string from input let Just x = parseInteger sx -- assuming int parse is ok, else error let Just y = parseInteger sy -- assuming int parse is ok, else error case decEq (x < y) True of -- decEq constructs a proof if x < y is True Yes prf => print (add x y prf) No => putStrLn "no prf, x is not less than y" lets say I mess up the sign of the comparison on the case line and write decEq (x > y) instead... then I'd get a type error When checking argument prf to function Main.add: Type mismatch between x > y = True (Type of prf) and x < y = True (Expected type) there's no way to construct the prf value artificially, or sneak in different parameters that are unrelated to the prf value. it's either a compile error or it's valid. c.f. https://news.ycombinator.com/item?id=12349384 https://news.ycombinator.com/item?id=12349384
dwohnitmok 9y ago
I'm very much a newbie when it comes to F# but as far as I can tell this isn't an example of what's traditionally called dependent types, but rather is a way of providing a set of helper functions and types for "smart" constructors, that is providing a validation/verification function that takes in some raw type and gives back an option of either the type you want or none. As a litmus test (and I'd be happy if either the OP or someone else chimes in), as an example of dependent types, I'd expect to be able to compose constraints, e.g. having a type called And<'A, 'B> and Or<'A, 'B> that would then let me compose constraints e.g. And<GreaterThan3, IsEven> and crucially have their verification functions automatically compose as well, instead of having to invent a whole new type GreaterThan3AndIsEven with a whole new verification function. As far as I can tell right now, that's not possible with this library and I need to go down the route of making the custom GreaterThan3AndIsEven type. Another good litmus test is whether literals also need to be passed through the verification function or not (or whether you have to pass them through the verification, get an option, and then unwrap the option with a comment indicating that it's safe to do so); for a usage of dependent types I would expect the answer to be no usage of the verification function would be required. The crucial thing that dependent types let you do is that you can manipulate types and values with many of the same tools. Composition (the and and or from above) is one hallmark of this ability. Another is being able to call a value-level function in a type signature. For example a type signature that looks like x : if (a + b == c) then Boolean else Int FWIW I don't mean to take away from this library; the practice of using smart constructors is something I'd love all expressively statically typed languages embrace wholeheartedly.
- jackfoxy 9y ago
  OP here. Since Martin-Löf type theory has introduced dependent types through the dependent function. No one I am aware of has improved on this approach, or even attempted a different way of introducing dependent types. And I think theory is very important. In Practice I think https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type gets it right in that dependent types exist independently of dependent functions. [A] dependent type is a type whose definition depends on a value. I think ordinary programmers solving ordinary problems benefit far more from the type safety dependent types provide than dependent functions or compile time creation checks. In ordinary programming most data is independent of the code. There are notable exceptions, of course. If in practical programming we may only ever use a term from computer science when it meets the CS definition in every way, I invite the reader to start a list of all the terms where this is already not the case. Also ordinary programmers are more likely to gain at least a superficial understanding of dependent types when every implementation of smart constructors does not call the resulting types something specific to that programming language, but otherwise unconnected to most anything else. Constructor composition is a neat idea and merits investigation. The idea of course springs from function (dependent function) composition. Not exactly what you are thinking, but I think somewhat related, take a look at the section Converting between dependent types in the tutorial https://jackfoxy.github.io/DependentTypes/tutorial.html https://jackfoxy.github.io/DependentTypes/tutorial.html
jpfed 9y ago
This is cool, but isn't it more like refinement types?
Tehnix 9y ago
From what I gather, this happens at runtime, which makes me feel it's a bit unfortunate to call it dependent types, or at least my view of dependent types is of it being a compile-time guarantee. Take for example Liquid Haskell[0] where you can, at compile time, make guarantees about your code. For example, here's a function that makes division safe, by never allowing the second value, y, to be 0, {-@ safeDiv :: Int -> {v:Int | v != 0} -> Int @-} safeDiv :: Int -> Int -> Int safeDiv x y = x `div` y The second annotation is plain Haskell meaning it takes 2 `Int`s and returns an `Int`, with the third line being the function body. The first {-@ .. -} annotation is the one Liquid Haskell reads, stating it takes an `Int` as the first argument, another `Int`, which we now refer to as v, that is not 0, and finally returns an `Int`. Another practical language with dependent types is Idris[1], which supports full dependent types with dependent pattern matching. Finally, for the "why would I use this", I recommend checking out Gabriel Gonsalez's keynote, from Haskell eXchange 2017, "Scrap your Bounds Checks with Liquid Haskell"[2] [0] https://ucsd-progsys.github.io/liquidhaskell-blog/ https://ucsd-progsys.github.io/liquidhaskell-blog/ [1] https://www.idris-lang.org https://www.idris-lang.org [2] https://skillsmatter.com/skillscasts/10690-keynote-scrap-your-bounds-checks-with-liquid-haskell https://skillsmatter.com/skillscasts/10690-keynote-scrap-you...
deleted 9y ago
[deleted]

136 points by jackfoxy 9y ago

Very cool library that Jack implemented here using an idea from my blog. We are using it in production. Works really nice.

deleted 9y ago
[deleted]

xyz-x 9y ago

Nice lib and library tests!

lkitching 9y ago

Does this library actually allow you to express dependent types or is it just for runtime validation? I can't see any examples in the documentation of a type depending on a value like the common let v : Vect 3 Int = [1,2,3] example. There aren't many types shown in the examples but it looks like let myNonEmptyIntSetOpt = [] |> Set.ofList |> NonEmptyIntSet.TryCreate would just return None at runtime rather than a compilation error?

jackfoxy 9y ago
How can you do a compile time check on data that has not entered the system? You can apply the same technique to Vect 3 [1,2,3] or any other type.
- jackfoxy 9y ago
  a dependent type is a type whose definition depends on a value https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type
- lkitching 9y ago
  How do you express the type `Vect 3 Int` using this library? F# doesn't support it and all the example types appear to depend on other types, not on values like 3.
  - jackfoxy 9y ago
    I'm pretty sure there are vector libraries available to F#. Dig around and you will find them. Then just apply dependent type to a type in that library. I don't work with them myself.
    - lkitching 9y ago
      I'm not asking specifically about vectors, that's just a common example of a dependent type. To take another example from the documentation, can you express a type like type digits = RegexString (Regex "^[0-9]+$") where all values of type digits are strings containing only digits? Then let s1 : digits = "1234" would typecheck but let s2 : digits = "abc" would not? That would be very surprising given the F# type system.
  - vorotato 9y ago
    Basically when you take some value the user gives you and cast it to the dependent type, you can then cover the case where you got some result because the cast was successful or you got none. You can't have dependent types at compile time, at least not completely so, though you could use something like fslint to catch any data being entered in code. https://news.ycombinator.com/item?id=7567310 https://news.ycombinator.com/item?id=7567310
    - vorotato 9y ago
      it would seem that in practice you can go even further, essentially writing exhaustive proofs. However F* already supports this and compiles to F#, so I would say if you want that level of correctness you should probably use a language which is better at describing the totality of a function.
- deleted 9y ago
  [deleted]
- cstrahan 9y ago
  > How can you do a compile time check on data that has not entered the system? You would have to supply proof that your types are correct; when you have a value who's type you'll only know at run time, you'll need to perform case analysis to bring additional info about the value's type into scope in the respective branches. To make concrete what I'm describing here, I'll use Idris's ++ (concatenation) as an example, which provides an inductive proof for the length of the resulting vector: (++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem (++) [] ys = ys (++) (x::xs) ys = x :: xs ++ ys The first line is the type signature, which claims that the length of the resulting vector is the sum of the lengths of the two argument vectors. The second line pattern matches on the null/empty constructor of the vector, and then returns ys. By pattern matching on the null constructor, we know that m == 0. We also know that n == length ys (whatever that may be). We know that 0 + x = x, so if we apply that to this case, we know that: length ([] ++ ys) == length [] + length ys == 0 + length ys == length ys == n == m + n (because we know m==0, and 0+n==n) ... so the compiler is happy here. The third and final line pattern matches on the non-empty (or cons, if you're a fan of Lisp) constructor. If this pattern applies, then we can make use of the fact that length (x::xs) == 1 + length xs. Of course, that that implies length xs < length (x::xs). That permits us to apply our induction hypothesis to the (xs ++ ys) sub expression, which tells that length (xs ++ ys) == length xs + length ys. Putting all of that together, we see that length (x :: xs ++ ys) == 1 + length (xs ++ ys) == 1 + length xs + length ys == 1 + (m - 1) + length ys == m + length ys == m + n That concludes our proof by induction[1]. Note that this proof is checked completely at compile time, and that it is still valid in the face of types which we won't know until we run our program. That's what dependent types give you. Here's an example that would not compile: (++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem (++) [] ys = ys (++) (x::xs) ys = x :: x :: xs ++ ys {- !!! note that I cons x here *twice* -} In conclusion, your library sounds like it could be an excellent way to provide smart constructors; at the same time, it's important to not conflate smart constructors with dependent types. I would urge you to continue developing your library, though I would recommend switching the name to something that's more indicative of what it actually does. That would have the additional benefit of not confusing people who read your project description and are hearing about dependent types for the first time. [1]: https://en.wikipedia.org/wiki/Mathematical_induction https://en.wikipedia.org/wiki/Mathematical_induction

Animats 9y ago

It's like subclassing, but it has to be called something else to be cool. Objects are so last-cen.

joeblubaugh 9y ago
It's significantly different than subclassing. The wikipedia examples are instructive: a dependent type is a type whose definition depends on a value. A "pair of integers" is a type. A "pair of integers where the second is greater than the first" is a dependent type because of the dependence on the value.
- Animats 9y ago
  That's a subclass with an object invariant. (Gotta use the new buzzwords to be l33t. Even for old ideas.)
  - joeblubaugh 9y ago
    Sure, so if you use Ada you can write types like this and the runtime will enforce your invariants automatically. What other non-academic languages support that? It’s something I miss from Ada for sure.
dwohnitmok 9y ago
You're right in that what's being demonstrated here should actually be old-hat for OO programmers. It's basically a factory that returns things wrapped in an option if pre-conditions fail. Crucially what's being demonstrated here isn't dependent types at least as they are commonly known (which some of the comments here explain). Dependent types are when expressions can not only be of a type, but can also return a type. That means for example something like x : (if condition then Boolean else Int) is a type, i.e. the entire thing within the parentheses to the right of the y. This is radically different from subclassing. That entire if statement is a type, not just the `Boolean` or `Int` parts. Indeed because now arbitrary expressions (in particular equality can return a type!) can return types, types can be statements of your program and simply getting the typechecker to accept the type proves properties of your program. x : 5 = 5 In here "5 = 5" is a type. This flips normal statically typed programming on its head. We care more about the type than the value! The actual value of "x" is probably not something you care about; it just proves (in this case the trivial statement) that "5 = 5." Less trivial equalities can be stated additionCommutes : (a : Int, b : Int) -> a + b = b + a and proved by providing a value for additionCommutes that satisfies the typechecker. Again the important thing is the entire right-hand-side of additionCommutes is a single type.

phillipcarter 9y ago

This looks neat!

HumanDrivenDev 9y ago

Is there a reason dependent types aren't more widely used? Is it just a case of people not wanting to learn anything new, or are there some show-stopping issues in practice? The idea seems promising. If I'm not mistaken it would let you statically declare that an integer had to be between values X and Y, for example.

skybrian 9y ago
Lack of compelling tutorials for beginners? The examples I've seen are either solving toy problems in a complicated way or not understandable at all.
- HumanDrivenDev 9y ago
  What's a toy problem in this case? Anything where you can replace even part of a dynamic contract seems like a win.
  - platz 9y ago
    > twblalock 468 days ago [-] > The Idris example seems to need further explanation: >> In Idris, we can say "the add function takes two integers and returns an integer, but its first argument must be smaller than its second argument": >> add : (x : Nat) -> (y : Nat) -> {auto smaller : LT x y} -> Nat >> add x y = x + y >That's all well and good, if you know the values of x and y at compile time. Consider a program that reads x and y from STDIN. The user could provide an x that is equal to or larger than y (or could provide only one value, or values that are not numbers). I see no way to deal with that except to throw a runtime error. Is that what would happen? In the case where the values are read from the external environment, first you would have to compare them before calling the function. The comparator would return either a proof that x <= y, or x > y. the proof ensures that at compile time you cannot mess this up. in other words, You have to perform the check at runtime, but the results for the check are enforced via a proof that is ensured to be correct at compile time. Connecting the proof the to the type system at compile time is the magic of dependent types > 18 points by platz 468 days ago [-] here's a full code example in Idris: import Data.String -- takes two integers, and a proof that x < y, and yields an integer add : (x : Integer) -> (y : Integer) -> (prf : x < y = True) -> -- require a proof that that x < y Integer add x y prf = x + y main : IO () main = do sx <- getLine -- read string from input sy <- getLine -- read string from input let Just x = parseInteger sx -- assuming int parse is ok, else error let Just y = parseInteger sy -- assuming int parse is ok, else error case decEq (x < y) True of -- decEq constructs a proof if x < y is True Yes prf => print (add x y prf) No => putStrLn "no prf, x is not less than y" lets say I mess up the sign of the comparison on the case line and write decEq (x > y) instead... then I'd get a type error When checking argument prf to function Main.add: Type mismatch between x > y = True (Type of prf) and x < y = True (Expected type) there's no way to construct the prf value artificially, or sneak in different parameters that are unrelated to the prf value. it's either a compile error or it's valid. c.f. https://news.ycombinator.com/item?id=12349384 https://news.ycombinator.com/item?id=12349384

dwohnitmok 9y ago

I'm very much a newbie when it comes to F# but as far as I can tell this isn't an example of what's traditionally called dependent types, but rather is a way of providing a set of helper functions and types for "smart" constructors, that is providing a validation/verification function that takes in some raw type and gives back an option of either the type you want or none. As a litmus test (and I'd be happy if either the OP or someone else chimes in), as an example of dependent types, I'd expect to be able to compose constraints, e.g. having a type called And<'A, 'B> and Or<'A, 'B> that would then let me compose constraints e.g. And<GreaterThan3, IsEven> and crucially have their verification functions automatically compose as well, instead of having to invent a whole new type GreaterThan3AndIsEven with a whole new verification function. As far as I can tell right now, that's not possible with this library and I need to go down the route of making the custom GreaterThan3AndIsEven type. Another good litmus test is whether literals also need to be passed through the verification function or not (or whether you have to pass them through the verification, get an option, and then unwrap the option with a comment indicating that it's safe to do so); for a usage of dependent types I would expect the answer to be no usage of the verification function would be required. The crucial thing that dependent types let you do is that you can manipulate types and values with many of the same tools. Composition (the and and or from above) is one hallmark of this ability. Another is being able to call a value-level function in a type signature. For example a type signature that looks like x : if (a + b == c) then Boolean else Int FWIW I don't mean to take away from this library; the practice of using smart constructors is something I'd love all expressively statically typed languages embrace wholeheartedly.

jackfoxy 9y ago
OP here. Since Martin-Löf type theory has introduced dependent types through the dependent function. No one I am aware of has improved on this approach, or even attempted a different way of introducing dependent types. And I think theory is very important. In Practice I think https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type gets it right in that dependent types exist independently of dependent functions. [A] dependent type is a type whose definition depends on a value. I think ordinary programmers solving ordinary problems benefit far more from the type safety dependent types provide than dependent functions or compile time creation checks. In ordinary programming most data is independent of the code. There are notable exceptions, of course. If in practical programming we may only ever use a term from computer science when it meets the CS definition in every way, I invite the reader to start a list of all the terms where this is already not the case. Also ordinary programmers are more likely to gain at least a superficial understanding of dependent types when every implementation of smart constructors does not call the resulting types something specific to that programming language, but otherwise unconnected to most anything else. Constructor composition is a neat idea and merits investigation. The idea of course springs from function (dependent function) composition. Not exactly what you are thinking, but I think somewhat related, take a look at the section Converting between dependent types in the tutorial https://jackfoxy.github.io/DependentTypes/tutorial.html https://jackfoxy.github.io/DependentTypes/tutorial.html

jpfed 9y ago

This is cool, but isn't it more like refinement types?

Tehnix 9y ago

From what I gather, this happens at runtime, which makes me feel it's a bit unfortunate to call it dependent types, or at least my view of dependent types is of it being a compile-time guarantee. Take for example Liquid Haskell[0] where you can, at compile time, make guarantees about your code. For example, here's a function that makes division safe, by never allowing the second value, y, to be 0, {-@ safeDiv :: Int -> {v:Int | v != 0} -> Int @-} safeDiv :: Int -> Int -> Int safeDiv x y = x `div` y The second annotation is plain Haskell meaning it takes 2 `Int`s and returns an `Int`, with the third line being the function body. The first {-@ .. -} annotation is the one Liquid Haskell reads, stating it takes an `Int` as the first argument, another `Int`, which we now refer to as v, that is not 0, and finally returns an `Int`. Another practical language with dependent types is Idris[1], which supports full dependent types with dependent pattern matching. Finally, for the "why would I use this", I recommend checking out Gabriel Gonsalez's keynote, from Haskell eXchange 2017, "Scrap your Bounds Checks with Liquid Haskell"[2] [0] https://ucsd-progsys.github.io/liquidhaskell-blog/ https://ucsd-progsys.github.io/liquidhaskell-blog/ [1] https://www.idris-lang.org https://www.idris-lang.org [2] https://skillsmatter.com/skillscasts/10690-keynote-scrap-your-bounds-checks-with-liquid-haskell https://skillsmatter.com/skillscasts/10690-keynote-scrap-you...

deleted 9y ago

[deleted]