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.)
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.
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.
Wow this is very exciting. If I understand correctly this effectively completes the Lambda Cube for F#.
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
Optionfor simple nullability.)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.
SomeandNoneare both values of the typeOption. 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 theOptiontype).Dependent types don’t end up in a language by accident, they’re something that has to be explicitly designed in.