Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Does Cidre have "top" refinements at non-datatypes? #15

Open
noamz opened this issue May 25, 2016 · 0 comments
Open

Does Cidre have "top" refinements at non-datatypes? #15

noamz opened this issue May 25, 2016 · 0 comments

Comments

@noamz
Copy link

noamz commented May 25, 2016

The grammar in section 7.8 of the thesis includes a "topsort [type]" construct, but it seems this is not legal syntax in the current version of Cidre. Am I right that Cidre only supports "top" refinements (0-ary intersections) for pure datatypes, and specifically that it does not have them for function types?

For example, suppose we begin by defining some function with a restricted domain:

(*[ datasort true = true ]*)

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

Now, I would expect the following code to fail to sort-check,

(*[ bad <: bool ]*)
val bad = idTrue false

and indeed Cidre gives an error:

  val bad = idTrue false
                   ^^^^^
  Sort mismatch: bool
      expecting: true

That makes sense: even though the sort bool is equivalent to the "top" refinement at type bool, we shouldn't be able to give idTrue false (which evaluates to an exception) the top sort due to the value restriction. However, if we had "topsort" at function types, then I would expect a thunked variation of this example to go through:

(*[ okaymaybe <: topsort[unit -> bool] ]*)
val okaymaybe = fn () => idTrue false

This is not (currently!) legal Cidre syntax, though. We could try the following:

(*[ alsobad <: unit -> bool ]*)
val alsobad = fn () => idTrue false

But this won't help (again the checker will complain), because the sort unit -> bool is not actually equivalent to the top refinement at type unit -> bool (and in general, we need not have that topsort[A -> B] = topsort[A] -> topsort[B] in the presence of effects).

Does this sound right? If so, then maybe you could read this as a feature request... ;-)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant