Type-safe vector addition with dependent types(chrisstucchio.com)
chrisstucchio.com
Type-safe vector addition with dependent types
https://www.chrisstucchio.com/blog/2014/type_safe_vector_addition_with_dependent_types.html
3 comments
In addition to using newtype wrappers, I think you can enforce the same thing via phantom types. Here's an example in Rust, showing this sort of approach being used in Servo: https://blog.mozilla.org/research/2014/06/23/static-checking...
Hm, I'm not sure this is directly connected to dependent types though? The example has
So I think this example is more about details of the Scala type system (nominal typing, coarseness of type equality) than about dependency as such.
val securityRepresentation = R(numSecurities)
val pcaRepresentation = R(numSecurities)
[error] found : securityRepresentation.V
[error] required: pcaRepresentation.V
So I think this example is more about details of the Scala type system (nominal typing, coarseness of type equality) than about dependency as such.
> securityRepresentation and pcaRepresentation are the same thing
Why? The path to V is obviously different, that's the whole point of it. If I wanted them to be the same, I wouldn't need to write it that way.
Why? The path to V is obviously different, that's the whole point of it. If I wanted them to be the same, I wouldn't need to write it that way.
I guess I was just surprised that the article was more Scala-specific than the title led me to expect.
Class types are generative. That's why p.V != q.V.
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#:
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:
Produces: val a : int<cm ^ 2> = 25
Andrew Kennedy calls these "Dimension Types": 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.