-
Notifications
You must be signed in to change notification settings - Fork 1
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
Support eliminating a variant with a record of functions with non-fixed codomain #12
Comments
mrkgnao
changed the title
Records of functions with non-fixed codomain don't seem to be legal
Support eliminating a variant with a record of functions with non-fixed codomain
Oct 22, 2017
That's a very unhelpful error message, isn't it? Though I suspect the
fundamental problem here is that the `.=` operator only supports the `I`
field structure, not others such as `I :->: I`.
```
(.=) :: L l -> t -> I l t
(.=) = const I
```
Your example needs an operator of type `L l -> (t -> t) -> (I :->: I) l t`
instead. `const coerce` implements that signature.
I'll see if the error message can be improved. Thanks again!
…On Sat, Oct 21, 2017, 23:47 Soham Chowdhury ***@***.***> wrote:
Consider the following type/term.
funcs :: R (I :->: I) (Row0 .& "int" .= Int .& "string" .= String)
funcs = mkR .* #int .= (\x -> 2 * x) .* #string .= reverse
This fails:
• Couldn't match type ‘(Row0 .& (l0 .= ())) .& (l1 .= ())’
with ‘(Row0 .& ("int" .= Int)) .& ("string" .= String)’
Expected type: R (I :->: I)
((Row0 .& ("int" .= Int)) .& ("string" .= String))
Actual type: R (I :->: I) ((Row0 .& (l0 .= ())) .& (l1 .= ()))
NB: ‘.&’ is a type function, and may not be injective
The type variables ‘l0’, ‘l1’ are ambiguous
• In the expression:
mkR .* #int .= (\ x -> 2 * x) .* #string .= reverse
In an equation for ‘funcs’:
funcs = mkR .* #int .= (\ x -> 2 * x) .* #string .= reverse
|
82 | funcs = mkR .* #int .= (\x -> 2 * x) .* #string .= reverse
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
<#12>, or mute the thread
<https://github.com/notifications/unsubscribe-auth/ABDg00RzxlSrYVPgD70atIGdiF8BceCBks5suuUAgaJpZM4QB1zz>
.
|
@nfrisby: apologies for the older version of the issue report. I was actually using I've updated the issue with what I was really trying to do. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
I'm not sure if there's something fundamental preventing the inclusion of a function of type
in
sculls
.One might then use a record of functions like
to eliminate a variant like
V I (Row0 .& "int" .= Int .& "string" .= String)
.The text was updated successfully, but these errors were encountered: