4 ms·

Type-safe vector addition with dependent types

39 points by djoldman 12y ago

kibwen 12y 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-of-units-in-servo/ https://blog.mozilla.org/research/2014/06/23/static-checking...
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.
vilhelm_s 12y 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 12y 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_s 12y ago
    I guess I was just surprised that the article was more Scala-specific than the title led me to expect.
- modersky 12y ago
  Class types are generative. That's why p.V != q.V.

39 points by djoldman 12y 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-of-units-in-servo/ https://blog.mozilla.org/research/2014/06/23/static-checking...

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.

vilhelm_s 12y 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 12y 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_s 12y ago
  I guess I was just surprised that the article was more Scala-specific than the title led me to expect.
modersky 12y ago
Class types are generative. That's why p.V != q.V.