1. 17
  1.  

  2. 2

    Wow this is very exciting. If I understand correctly this effectively completes the Lambda Cube for F#.

    1. 4

      It doesn’t. This has very little to do with dependent types, but are more like smart constructors.

      Here’s a translation into boring old C# to show that nothing particularly F#-specific (or very fancy at all, given C#‘s type system) is going on at the type level. (I’ve switched out Option for simple nullability.)

      1. 1

        Actually they are by definition dependent types. They maybe aren’t the most sophisticated dependent types…. but

        “A function whose type of return value varies with its argument is a dependent function and the type of this function is called dependent product type, pi-type or simply dependent type.” In your case using a null there doesn’t satisfy this definition because null is a value included in your type. I however do agree, this can be implemented in all kinds of languages and yes is basically a constructor that throws one type if it’s valid and another type if it is not. What matters mostly is how cumbersome the syntax is and that you can have a type for a parameter that always meets your condition there. You KNOW that because it is a PositiveInt, it has a value, and that that value is greater than 0 and you do not need to check for it within the function that takes a PositiveInt as an argument. The type depends on the value.

        1. 1

          In your case using a null there doesn’t satisfy this definition because null is a value included in your type.

          Some and None are both values of the type Option. You can similarly translate this into C# but I couldn’t be bothered (at the CLR level the F# values translate into sub-classes of the Option type).

          Dependent types don’t end up in a language by accident, they’re something that has to be explicitly designed in.