Skip to content

drop type safety in the implementation, interface is still safe#35

Merged
EmileTrotignon merged 6 commits into
Drup:masterfrom
EmileTrotignon:noexpr
Nov 12, 2025
Merged

drop type safety in the implementation, interface is still safe#35
EmileTrotignon merged 6 commits into
Drup:masterfrom
EmileTrotignon:noexpr

Conversation

@EmileTrotignon
Copy link
Copy Markdown
Collaborator

This is because:

  • The value restriction can only be relaxed with covariant type parameters.
  • GADT parameters can only be covariant if they are not specialised, that is if they are used as in a regular ADT
  • Values like int need type ('e, int) t because otherwise int <&> map f ... does not type.

The only solution I have is to drop the type safety around evaluability. The .mli is still safe, except for the Internal module.

Extra care has to be put in making the mli safe in the future

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

Successfully merging this pull request may close these issues.

1 participant