Dependent Types for F# | Hacker News Reader

Dependent Types for F#

jackfoxy.github.io

136 pointsjackfoxy51 comments

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.

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

I agree with I think what you're hinting at with regards to practicality. It is definitely the case that using this library or the practices that it espouses is far more practical for the working programmer than to try to get people to rework rewriting their codebase in Coq.

That being said, if I understand this library correctly, I strongly disagree with the choice to call it "Dependent Types." There's certainly no inherent reason that a cabal of type theorists should have a monopoly on the word "dependently typed," but I think describing this library as dependently typed dilutes the meaning of this word beyond usefulness. The crucial idea behind this library can be implemented in every statically typed language I know of (essentially anything that supports hiding certain constructors and exposing alternate ones and using some sort of optional type to represent failure rather than blow up at runtime). The specific implementation details of storing all the functions together can certainly be approximated in every statically typed FP language I've used (which is not to say it isn't valuable or a unique take on the problem!). Under what I think is your definition of dependent types, Java is a dependently typed language, which really starts muddying the waters for programmers trying to learn this stuff. This has two main drawbacks.

1. It obfuscates what this library is doing to programmers who have not used dependent types before. The mix of questions in this very HN thread, some of which are more appropriately directed at a language like Idris, is a testament to that. Once again depending on whether I understand this library correctly, this library seems to be an extension of the idea of having separate public and private constructors for types and codifying the public constructors for a type. This is something that I would wager most working programming have some familiarity with and can immediately understand its usefulness instead of having to ask around (and get irrelevant answers) about what dependent types are.

2. It disappoints and confuses people who have used dependent types. Honestly it comes off as buzzword marketing. An analogy would be if someone took the C language and added a new word "class" that was a synonym for "struct," did absolutely nothing else, then proclaimed that C was object-oriented (a term which is far less well-defined than dependently typed). "Ah so do your new C OO classes support inheritance?" "Nope." "Hmmm... so do you have methods?" "Nope." "Well then they aren't really classes and it feels disingenuous to call them such... (unlike e.g. how C++ extends the semantics of struct)."

If what you're talking about RE Martin-Löf type theory and the dependent function are pi and sigma types sure that's the formal treatment of dependent types, but I'd argue that there's a simpler working definition that suffices for most cases. A dependently typed language is simply a language where expressions not only can have a type, but can evaluate to a type. Hence my "if ... then ..." example from earlier.

I think the most accurate, widely-used term that describes what's going on here is the factory pattern. Simple as that and I think that's familiar enough to most programmers.

Upon re-reading this comment, I want to say that I don't think this library is trivial (it's not "just" the factory pattern) and that it is definitely a valuable way of structuring a given pattern! I know putting something on HN is a great way of getting crowds of know-it-alls to heckle and discourage you so I hope I haven't done that, just wanted to point out something that was bothering me.

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/

[1] https://www.idris-lang.org

[2] https://skillsmatter.com/skillscasts/10690-keynote-scrap-you...

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?

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.

a dependent type is a type whose definition depends on a value https://en.wikipedia.org/wiki/Dependent_type

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.

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

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.

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.

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.

> 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

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.

I think it's two things. The first one is that most people are not comfortable changing up the programming paradigm that they are most familiar with. They're familiar with adding some if-statements to verify at run time. They're not familiar with using the type system to prove the properties of their data. Proving non-trivial properties can be hard (and in some cases impossible), so it makes sense that few people are jumping at the opportunity to learn everything from the ground up all over again when the alternative is to just use an if-statement.

The second thing is that sometimes you're going to get dynamic data at run time and you're going to have to use a run time property checker anyways. So for example if you needed to parse a bunch of text sent in by the user. You can still use dependent types to offload as much as possible to the type system, but at some point you'll have to deal with receiving user data. And if we go back to my first point, people are uncomfortable with using new things. They won't have a good idea of when to put what into the type system and what into the run time, so the default will be to just do it all at run time.

Liquid types look kind of promising, but I'm not sure if it's still an active research area. The stuff rust is doing with affine types is also promising. It's not dependent, but you can make a bunch of very nifty compile time checked apis. Finally, ML style types are slowly becoming more familiar in general in the industry. Once everyone is fully familiar with type parameters, they'll start to ask about kinds and values in types. However, it may take a while.

> You can still use dependent types to offload as much as possible to the type system, but at some point you'll have to deal with receiving user data.

Of course you have do deal with receiving data at run time, but I think very few people appreciate that it's actually possible to do the "input verification" at one specific point in your program and then have a "proven" safe input and then never have to do any validation/verification again. This even goes for things like "give me a vector of integers between 1 to 3 of size exactly 9 as input". Of course you still have to handle the invalid cases in that one specific place, but that's no different from how you'd ideally do validation anyway. That stuff already should be in a single place, and dependent types make that utterly obvious at compile time :).

(I think I may actually be agreeing with what you're saying, but I though it worth expounding on what dependent types can do for you.)

Btw, AFAIUI Liquid Types, at least as far as LiquidHaskell goes, is still a thing, though it's definitely quite "researchy" and who knows whether it'll become 'mainstream'.

Liquid Types also seem to be somewhat orthogonal to dependent types since they usually just rely on an external solver that works by "magic" (SMT) and which has built-in knowledge of e.g. arithmetic whereas most attempts at dependent types seem to want to avoid building in any of that knowledge in favor of induction + a more general "tactics" or "elaboration" type solving where the programmer guides the solver along. (Idris is an example of the latter, I think.)

Your last point is interesting - I believe Idris and/or Agda in fact go out of their way to show a natural number type defined using induction as a key example. I remember being blown away by that.

Coming from dynamic languages towards appreciation of static types, this sort of thing is inspiring. I've been looking forward to writing some practical work in those languages when children and time give the chance.

> it's actually possible to do the "input verification" at one specific point in your program and then have a "proven" safe input and then never have to do any validation/verification again.

This can be done with "tainting" types, which are simple intersection types (even Java has them as one of its new pluggable type systems [1]), and doesn't require dependent types.

[1]: https://checkerframework.org/manual/#tainting-checker

It's useless if it's optional.

So is F#.

Assuming you mean “dependent types in F#” rather than “F#”, after reading the article, I concluded that these are, in fact, not dependent types, but just so-called “smart constructors”. Since “dependent types in F#” don't exist, it doesn't make sense to ask whether they're useful or useless.

I meant that F# itself is optional. So are tests, by the way, and therefore also completely useless.

Yeah, F# is kind of problematic since you aren't forced to use F# to typefully use F# libraries. Things would be a lot better in a language like Standard ML, where you can either use a library correctly (assuming it exposes the right interfaces) or not use it at all. Hooray for abstraction!

There really does seem to be a Last Mile problem with a lot of these systems for formalism.

You're going to get garbage data from paying customers. With a good information architecture you'll have 'lines' in the system and all of the data that goes past a certain point is guaranteed to be sanitized, at which point all this formalism helps you avoid really bad mistakes.

What ends up happening most times is a set of proprietary bespoke thunking layers that progressively sanitize the data until its usable. Everybody writes their own and they either suck or took lots of effort to get right. Or, the entire system is full of uncertainty and reads like a Choose Your Own Adventure as written by a squirrel.

Maybe there's a space there between the user and the formal type system that needs a set of transformation tools. Like htmltidy, but without the html.

One of the core issues is that arbitrary dependent types require writing difficult formal proofs [0]. Xavier Leroy, who, as the main author of CompCert -- probably the only non-trivial program proven end-to-end [1] with the use of a proof assistant based on dependent types -- has often said that even he, a world expert, had found this so laborious that he views manual proofs as viable only to small programs (and CompCert, while non-trivial, is certainly a small program). Short of that, the question is exactly how useful it is to prove only those properties that are easy to prove. Another issue is that there may be better alternatives (which could be combined with restricted, "easy", forms of dependent types. Contract systems (like Java's JML), are as expressive as dependent types, but separate specification from verification, meaning, they allow you to state program properties formally, and then use either (expensive) formal proofs or weaker forms of verification (like generated tests) to verify them. Proofs are both extremely costly and are very rarely a requirement; their added confidence beyond other, weaker, but far cheaper, forms of verification is very rarely worth their tremendous cost.

[0]: See this example of a simplified Quicksort in Idris: https://github.com/bmsherman/blog/wiki/Quicksort-in-Idris

[1]: End-to-end verification is ensuring that global correctness properties (e.g., "the database is always consistent", or "no user ever gets access to another's data") are preserved all the way to source code or even to machine-code. Most "formally verified" software, at least in industry, isn't verified end-to-end. Rather, either global properties are verified not against the code but a high-level description of the software or only local properties are verified at the code level, or both (but with a gap).

Have you seen CakeML[0]? It is verified that the semantics of the x86 machine code it outputs in the end are the same as the SML code it takes as input, up to out-of-memory errors.

[0]: https://cakeml.org/

I guess the main reason is the lack of mapping to actual world cases.

Usually you have tutorials about peano numbers and such, instead of how do I show a set of data records, straight out of a PostgreSQL database.

So far, Type-Driven Development with Idris, seems to be the best book for real world cases, and even it might a bit over the top for the common CRUD developer.

I think it's a an practicality thing. Getting these systems powerful seems sorta solved, but getting them easy to use seems tricky. AFAIK it's similar to computer formalized proofs. We can do them, but it's super verbose and tricky to make it convenient enough to be worthwhile.

Ada has always had integer ranges. Dependent types include integer ranges, but integer ranges aren't necessarily dependent types.

Dependent types do a bit more than that. Supposing you want to put a random pixel on a canvas C, but you don't know C's dimensions at compile time (perhaps because the user can change them at run time). The numerical value of the pixel's x and y coordinate ranges aren't known at compile time, but it is known that they're not negative and less than C.width and C.height.

    C = new Canvas
    ...

    // random(n) returns an integer of type range(0, n)
    x = random(C.width) // x has type range(0, C.width)
    y = random(C.height) // y has type range(0, C.height)

    // drawPoint(w, j, i) takes args of type canvas, range(0, w.width), range(0, w.height).
    drawPoint(C, x, y) // The types of x and y depend on the run-time value of C.

Using dependent typing would enable us to remove another source of bugs.

> Ada has always had integer ranges. Dependent types include integer ranges, but integer ranges aren't necessarily dependent types.

I was under the impression that Adas integer ranges were checked at runtime, like contracts. Is that not the case?

That's correct, it's a run-time check. According to https://en.wikibooks.org/wiki/Ada_Programming/Types/range

    A range is a signed integer value which ranges from a 
    First to a last Last. It is defined as

        range First .. Last

    When a value is assigned to an object with such a range 
    constraint, the value is checked for validity and 
    Constraint_Error exception is raised when the value is 
    not within First to Last.

Right. I said dependent types would allow you to statically declare integer ranges, as is my understanding.

It's interesting to me how Ada takes the approach of blending types and run time contracts. In most languages it would be two different things - a function that takes int, then a contract or assert that handles the value.

Some Lisp implementations (like SBCL) also do that blending, although they can statically catch some integer range violations too. For example if you declare a variable to be an (integer 50 100) and try to assign a literal 30 to it, you'll get a compile-time warning in SBCL:

    ;   Constant 30 conflicts with its asserted type (INTEGER 50 100).

But in many other cases it'll generate a runtime check instead, because the static type checking is basically best-effort.

They allow you to statically declare integer ranges (as well as other things), even if their bounds are unknown until run-time, and without requiring a run-time type check.

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.

What's a toy problem in this case? Anything where you can replace even part of a dynamic contract seems like a win.

It may or may not be a win. If the constraint being validated is trivial and the complexity added is substantial then maybe it's not a win?

A common example for demonstrating dependent types seems to validating the length of a list, but they don't show how it's useful in a problem where validating the length is important (for example to prevent security issues).

Also, a good example would be performing a calculation on external input data (from user input, a file, or a network connection), rather than on a constant, and showing how invalid input is handled.

> 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

How to use dependent types in practice is still a research topic. There’s some interesting problems with having a Turing powerful type system. Like type equality doesn’t work the same way.

you can do that in a function preamble (constructor), too. Dependent types are derived from higher order logic, a thing many programs simply don't need if they are straight up first order logic in essence and the use would be constrained to refactoring for DRY KISS principles, but dependent types are probably not simple in comparison.

> you can do that in a function preamble (constructor), too.

Well, yeah, but that's a runtime failure. Obviously that's heaps better than just failing at some arbitrary later time, but if might be better still to force the program writer to consider up front what should happen if construction were to fail.

In the particular case of preconditions for constructing data I would say that constructor validation is usually sufficient for my purposes, at least. I routinely use it in Haskell (abstract newtypes) and it seems to work fine, especially when you couple it with general validation (REST services).

EDIT: I should mention: What I personally find very attractive about fully dependently typed languages is the fact that you, the programmer, get to choose exactly how much you want to prove. Want to work with a JSONValue which can be any old JSON? Sure, you can do that! Want to work with a JSONValue which must contain (at least) keys 'foo' and 'bar' which map to data of type 'Foo' and 'Bar' at all times? Sure you can do that too!

(JSON may not be the best example, but I hope you get the meaning.)

Of course type inference suffers a bit, error messages probably too. However, I don't see that as a huge problem. YMMV.

If you're talking about the restricted/smart constructor approach that I think is exemplified by this library, i.e. the approach that hides the construction of a type behind a mandatory verification function, it's a pattern that's been around for a long time. OOP constructors are perhaps the best known example, although they often through an exception on invalid input rather than represent this at the type level with an Option/Maybe type or Either type.

I personally think that this approach (with the type level tracking) is indeed woefully underused (and is an easy-to-understand-and-implement win in most codebases) and would usually chalk it up to lack of familiarity in the community.

That being said, there are definitely domains that can make this approach (without the help of general dependent types) cumbersome to the point that I would consider scrapping it. One example of this is doing statistics and collection types. Most statistical operations operate over a collection of values. This is easily supplied by a standard collection type such as List or Vector. A significant chunk require a non-empty collection of values (think aggregate statistics such as mean). A type such as NonEmptyList or NonEmptyVector comes in handy here along with the corresponding verification function. A smaller chunk require collections of at least two elements (e.g. a sample estimate of standard deviation). Now you need a separate AtLeast2ElemList with a separate verification function. Estimates of higher statistical moments that are used with ever-decreasing frequency the higher you go up require at least 3, 4, etc. elements in a collection. Now you need an AtLeast3ElemList, an AtLeast4ElemList, etc. set of types with all their corresponding distinct verification functions. That's a lot of pain for little gain. In practice I usually personally handle this with covering 90% of cases with a collection and NonEmptyCollection type and then in those other cases have the aggregation function take a general collection and return an optional value rather than enforce GreaterThanN-ness at the input type. This is where dependent types could step in and have a single function AtLeastNElems with a single corresponding verification function and cut down on this madness.

Which brings me to general dependent types. If you're talking about general dependent types, the answer is the ergonomics are hard and best practices are still nascent. Coq, Agda, ATS, and Idris are all examples of dependently typed languages, but none of them are close to mainstream. Part of that is because they just haven't had close to the resources devoted to them that mainstream languages have had. Part of that is because some aspects of using them are still somewhat open programmer UX problems. Because you can write any sort of total function in a type signature you have to worry about a couple of things.

1. Compile times. You're doing complex stuff with complex types. It will always be true that you can create pathologically long compile times (this is true in most type systems far weaker than dependent types). What will make or break your type system is if the pathological cases come up regularly in normal code (sad case) or if a user has to create some really messed up code in order to hit those cases (happy case). This is even harder to get right if you give users a ton of rope when it comes to types.

2. If you're not careful not only can you verify, you must verify. It is often the case in a dependently typed language that you will use part of a type to provide a value used in a computation. E.g. a type of GreaterThanX might embed a comparison function that then gets used later in the computation of a value. Most languages have some notion of a "BelieveMeThisIsTrue" value which can be of any type and blows up at runtime if it actually ends up getting called. This functions as an escape hatch that lets you circumvent any type checks because you can always submit this value and have everything type check. You might hope that whenever the burden of verification gets too high, you can just submit "BelieveMeThisIsTrue" if you're sure that some property is true and omit any necessary checks. However, if you've embedded a value-level computation that you are planning to use later on in the type, then "BelieveMeThisIsTrue" will blow up your whole program, e.g. when you go to use the comparison function you've embedded in your GreaterThanX type. This means that you gotta make sure that verification is pretty easy or that it's pretty hard to end up forcing mandatory verification with absolutely no escape hatch. Both are hard problems.

Dependent types are extremely exciting, but finding the best way of using them in practice is still something of a research problem.

So far the nicest applications of them have been in restricted domains where you don't get the full power of dependent types, which limits their expressiveness, but makes it a lot easier to get the programmer ergonomics right See projects such as LiquidHaskell (https://ucsd-progsys.github.io/liquidhaskell-blog/) or Cryptol (https://cryptol.net/).

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

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

Nice lib and library tests!

This looks neat!

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

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.

That's a subclass with an object invariant.

(Gotta use the new buzzwords to be l33t. Even for old ideas.)

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.

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.

Reply on news.ycombinator.com