search

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

understanding the value restriction on intersections #16

Closed noamz closed 8 years ago

noamz commented 8 years ago

Consider:

(*[ datasort true = true ]*)

(*[ f <: true -> true list ]*)
fun f true = [true]

(*[ g <: true -> true ref ]*)
fun g true = ref true

(*[ passes <: true list & bool list ]*)
val passes = f true

(*[ fails <: true ref & bool ref ]*)
val fails = g true

Naturally, the unsafe annotation fails <: true ref & bool ref fails...

  val fails = g true
              ^^^^^^
  Sort mismatch: true ref
      expecting: true ref & bool ref

but I was a bit surprised that the safe annotation passes <: true list & bool list passes the sort-checker, even though the definition of passes syntactically violates the value restriction.

Is there a simple explanation for what exactly Cidre is doing? I guess it probably has something to do with the fact that the sort true list (which can be synthesized for the application f true) is a subsort of true list & bool list, but the sort true ref is not a subsort of true ref & bool ref?

noamz commented 8 years ago

Nevermind, from your thesis it's pretty clear that that's exactly what's going on: the expressions f true and g true are inferrable terms, so they synthesize sorts, and Cidre just has to check that those sorts are subsorts of the annotations.