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

Weird types when masking read,write,alloc effects #520

Open
anfelor opened this issue May 14, 2024 · 0 comments
Open

Weird types when masking read,write,alloc effects #520

anfelor opened this issue May 14, 2024 · 0 comments

Comments

@anfelor
Copy link
Collaborator

anfelor commented May 14, 2024

For mask<read>, Koka infers the following type signature:

fun mask-read(f : () -> <alloc<h>,write<h>|e> a) : e a
  mask<read>{ f() }

I am quite surprised by that and would have expected the type signature:

fun mask-read(f : () -> e ()) : <read<h>|e> ()
  mask<read>{ f() }

However, Koka can not compile this:

Type.InferMonad.runUnify: should never fail!: NoMatch
CallStack (from HasCallStack):
  error, called at src/Common/Failure.hs:46:12 in koka-3.1.1-GrUKw6cowJ9E7PPCKFMvzQ:Common.Failure
  raise, called at src/Common/Failure.hs:32:5 in koka-3.1.1-GrUKw6cowJ9E7PPCKFMvzQ:Common.Failure
  failure, called at src/Type/InferMonad.hs:653:17 in koka-3.1.1-GrUKw6cowJ9E7PPCKFMvzQ:Type.InferMonad

Koka accepts the definition:

fun mask-write(f)
  mask<write>{ f() }

and tells me that the type is fun mask-write : forall<a,h,e> (f : () -> <alloc<h>,read<h>|e> a) -> e a. However, Koka does not accept the definition with this signature:

fun mask-write(f : () -> <alloc<h>,read<h>|e> a) : e a
  mask<write>{ f() }

and fails with:

effects do not match
context        : fun mask-write(f : () -> <alloc<h>,read<h>|e> a) : e a
                   mask<write>{ f() }
term           :                                                      
                   mask<write>{ f() }
inferred effect: <write<_h>,alloc<$h1>,read<$h1>|$e>
expected effect: $e

In contrast to those cases, Koka does the right thing for alloc:

fun mask-alloc(f : () -> e a) : <alloc<h>|e> a
  mask<alloc>{ f() }

For completeness, these are the signatures of composing the masks:

fun mask-read-write(f : () -> <alloc<h>|e> a) : e a
  mask<read>{ mask<write>{ f() }}

fun mask-read-alloc(f : () -> <write<h>|e> a) : e a
  mask<read>{ mask<alloc>{ f() }}

// This definition gives a type error for wrong signature,
// but infers exactly this signature when none is given
// (like for the plain mask<write> above):
fun mask-write-alloc(f : () -> <read<h>|e> a) : e a
  mask<write>{ mask<alloc>{ f() }}

fun mask-read-write-alloc(f : () -> e ()) : e ()
  mask<read>{ mask<write>{ mask<alloc>{ f() }}}

Notice in particular that masking all these effects in the identity. In particular, this prevents us from writing a custom version of the mask<st> operator requested in #155. I could imagine that this is caused by implicitly trying to apply the run operation?

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

No branches or pull requests

2 participants