Type-safe vector addition with dependent types

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/Di...

But the F# implementation is not extensible to arbitrary types, and only works on built-in numbers.

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

    val securityRepresentation = R(numSecurities)
    val pcaRepresentation = R(numSecurities)

and gives the error

    [error]  found   : securityRepresentation.V
    [error]  required: pcaRepresentation.V

But securityRepresentation and pcaRepresentation are the same thing! If the Scala typechecker was more agressive, it could deduce that these types are equal. (And in a pure language like Coq and Agda, this would compile).

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.