3 ms·
Dependent types seem to be usually aimed at things like statically checking the sizes of arrays. At least, that's where I've heard of them. And the verbosity ha
by MichaelGG 12y ago
Dependent types seem to be usually aimed at things like statically checking the sizes of arrays. At least, that's where I've heard of them. And the verbosity has been a killer issue every time, in addition the the fact that you're often going to have dynamically sized types and going to have to cast anyways.
This kind of thing in the article is easy to do via a generic sum type using a phantom type (type that appears on left but not right). In F#:
type Id<'a> = Id of int
type AccountId = Id<Account>
let aid : AccountId = Id 4
A common example is in Html, having a String<HtmlEncoded> versus String<Raw>. It'd be nice if more languages made it simple to add on phantom type parameters, without the hassle of having to take around a type parameter every time you touch such a type. That is, any code written for plain String should seamlessly work for String<Foo>.
Of course unwrapping them is a bit of a pain. F# has units of measure, which specially apply to numbers. They take it a step further and propagate the operations you do to the number to the type:
[<Measure>] type cm
let h = 5<cm>
let a = h * h;;
Produces:
val a : int<cm ^ 2> = 25
Andrew Kennedy calls these "Dimension Types": http://research.microsoft.com/en-us/um/people/akenn/units/DimensionTypes.pdf http://research.microsoft.com/en-us/um/people/akenn/units/Di...
But the F# implementation is not extensible to arbitrary types, and only works on built-in numbers.