Type-safe vector addition with dependent types

https://www.chrisstucchio.com/blog/2014/type_safe_vector_addition_with_dependent_types.html

by djoldman • 12 years ago

39 6 12 years ago

kibwen• 12 years ago

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

MichaelGG• 12 years 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/Di...

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

vilhelm_s2• 12 years ago

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.

frowaway001• 12 years ago

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.

vilhelm_s2• 12 years ago

I guess I was just surprised that the article was more Scala-specific than the title led me to expect.

modersky• 12 years ago

Class types are generative. That's why p.V != q.V.

Type-safe vector addition with dependent types

Related Stories