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.

Sign up for GitHub

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

Jump to bottom

Extraction reports type mismatches due to type aliases for function types #51

Closed
tchajed opened this issue Aug 4, 2017 · 3 comments
Closed

Extraction reports type mismatches due to type aliases for function types #51

tchajed opened this issue Aug 4, 2017 · 3 comments

Comments

@tchajed
Copy link
Contributor

tchajed commented Aug 4, 2017

f doesn't extract to C in the following example due to a type mismatch between bool and bool_function () == bool -> bool. I'm not sure where that comes from, but adding unfold to the alias bool_function fixes the issue, at the cost of affecting verification.

module Type_alias

open FStar.HyperStack
open FStar.HyperStack.ST

(* this unfold is required to get f to extract correctly, but is undesirable
from a verification perspective *)
// unfold
let bool_function (spec: nat -> nat) = bool -> St bool

let f (y:bool) : bool_function (fun x -> x) =
  fun x -> x && y
@jkzinzindohoue
Copy link
Contributor

As far as I know, Low* does not support higher order and partial application, so I would not expect this to extract to C.

tchajed added a commit to FStarLang/FStar that referenced this issue Aug 4, 2017
@tchajed
Inline definitions while computing ML types
879fc34 
Fixes FStarLang/karamel#51
@tchajed tchajed mentioned this issue Aug 4, 2017
Merged
@tchajed
Copy link
Contributor Author

tchajed commented Aug 4, 2017

Well after unfolding bool_function it's clear that f can be extracted to a two-argument function, which is exactly what happens with unfold.

We've discussed an example like this in the context of my key-value store parsing experiments and decided that inline_for_extraction on bool_function (which currently can't really have any impact) should have the behavior unfold currently does, except that it would only apply to extraction and not verification.

@msprotz
Copy link
Contributor

msprotz commented Aug 8, 2017

What happens is probably along the lines of: the definitions of the bool_function type, for some reason or another (most likely the fact that it mentions nat) is not expressible in Low*. The net result is, applications of bool_function to its erased argument unit remain, but the missing definition of bool_function prevents these applications from expanding into bool -> bool, hence the error message.

inline_for_extraction on the type definition is indeed the right way to solve this.

If you want to improve the error message, or possibly write some of the things you're learning in MANUAL.md, then by all means feel free to edit...

Thanks,

Jonathan

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@tchajed @jkzinzindohoue @msprotz