ARRAY and VECTOR don't match the standard basis

rowandavies / sml-cidre

SML Checker for Intersection and Datasort Refinements (pronounced "cider")

http://www.cs.cmu.edu/~rowan/sorts.html

Other

20 stars 2 forks source link

ARRAY and VECTOR don't match the standard basis #12

Closed rowandavies closed 12 years ago

rowandavies commented 12 years ago

The ARRAY and VECTOR signatures are pretty clearly out of date.

Also, the default refinement of 'a vector isn't covariant when it should be. (But obviously not for 'a array!) The same is probably true for other type constructors that are opaque in the standard basis signatures.

Also, are there any other of the signatures related to "basic" (compiler implemented) types that haven't been properly compared to the standard basis spec?

rowandavies commented 12 years ago

Fixed in https://github.com/rowandavies/sml-cidre/commit/36dedfcda6d3b5d6281456e2965a455ecc7155a7