3 ms·
Hm, I'm not sure this is directly connected to dependent types though? The example has val securityRepresentation = R(numSecurities) val pcaRepresentat
by 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 agoI guess I was just surprised that the article was more Scala-specific than the title led me to expect.
- modersky 12y agoClass types are generative. That's why p.V != q.V.