test: add tests for associated type multiple Effs and types
#7555
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
@mlutze can you help me pinpoint the instance error? I really don't see how this is a valid instance error. mod Test.Dec.Assoc.Type.Eff.Multiple {
////////////////////////////////////////////////////////
// Type Definitions //
////////////////////////////////////////////////////////
eff Observe {
pub def captureInt32(x: Int32): Unit
pub def captureString(x: String): Unit
}
enum Split[e: Eff, a: Type] {
case Nothing,
case Value(a),
case Pending(a -> Unit \ e, a)
}
trait Composable[a] {
pub type E: Eff
pub type B: Type -> Type
pub type C: Eff -> Type -> Type
pub def compose(f: a -> Unit \ Composable.E[a], x: a): Composable.C[a][Composable.E[a], Composable.B[a][a]]
pub def reduce(x: Composable.C[a][Composable.E[a], Composable.B[a][a]]): Composable.B[a][a] \ Composable.E[a]
}
instance Composable[Vector[a]] with Composable[a] {
pub type E = Composable.E[a]
pub type B = Vector
pub type C = Split
pub def compose(f: Vector[a] -> Unit \ Composable.E[a], x: Vector[a]): Split[Composable.E[a], Vector[a]] =
Split.Pending(f, x)
pub def reduce(x: Split[Composable.E[a], Vector[a]]): Vector[a] \ Composable.E[a] = match x {
case Split.Nothing => Vector#{}
case Split.Value(v) => v
case Split.Pending(f, v) => f(v); v
}
}
} |
|
I think it is because of the |
|
Ah thanks! :) |
|
Okay so now it says that it is an irreducible associated type. Is it because of the recurrence of |
Irreducible shouldn't happen anymore, so it's probably a bug. Can you post the new program and the error message? |
|
Ah I was on latest release rather than |
jaschdoc
commented
Apr 8, 2024
|
@jaschdoc Is this blocked or OK? |
No I don't believe so. Just haven't finished writing everything. I think I was reconsidering the design. |
8 tasks
|
Error trait Transformable[a] {
pub type E: Eff
pub type B: Type
pub def transform(x: a): Transformable.B[a] \ Transformable.E[a]
}
pub def transformAndCheckEq[b](eq: Transformable.B[a], x: a): Bool \ Transformable.E[a] with Transformable[a], Eq[b] where Transformable.B[a] ~ b =
Transformable.transform(x) == eq
|
|
Error trait Composable[a] {
pub type E: Eff
pub type B: Type -> Type
pub type C: Eff -> Type -> Type
pub def compose(f: a -> Unit \ Composable.E[a], x: a): Composable.C[a][Composable.E[a], Composable.B[a][a]]
pub def reduce(x: Composable.C[a][Composable.E[a], Composable.B[a][a]]): Composable.B[a][a] \ Composable.E[a]
}
pub def composeAndReduceEq[a: Type](eq: Composable.B[a][a], f: a -> Unit \ Composable.E[a], x: a): Bool \ Composable.E[a] with Composable[a], Eq[a] where Composable.B[a] ~ a =
Composable.reduce(Composable.compose(f, x)) == eq
|
jaschdoc
commented
Apr 19, 2024
| // Polymorphic functions using Composable // | ||
| //////////////////////////////////////////////////////// | ||
|
|
||
| pub def composeAndReduceEq(eq: Composable.B[a][a], f: a -> Unit \ Composable.E[a], x: a): Bool \ Composable.E[a] with Composable[a], Eq[a] where Composable.B[a][a] ~ a = |
There was a problem hiding this comment.
I'm stuck on this function. Not sure how to resolve this:
❌ -- Syntax Error -------------------------------------------------- file:///.../TestEffMultiple.flix
>> Illegal equality constraint.
126 | pub def composeAndReduceEq(eq: Composable.B[a][a], f: a -> Unit \ Composable.E[a], x: a): Bool \ Composable.E[a] with Composable[a], Eq[a] where Composable.B[a][a] ~ a =
^^^^^^^^^^^^^^^^^^^^^^
Equality constraints must have the form: `Assoc[var] ~ Type`.
There was a problem hiding this comment.
The where clause can never be true. Imagine Composable.B[a] is defined as List. Then we are trying to unify List[a] ~ a which is impossible.
There was a problem hiding this comment.
So is it impossible to do what I'm trying to achieve?
There was a problem hiding this comment.
At least for that constraint, yes.
Does this not work without the constraint?
There was a problem hiding this comment.
I need equality on the type C where C is the associated type of an instance for B which again is an associated type for an instance for A if that makes sense?
There was a problem hiding this comment.
That makes me happy haha
There was a problem hiding this comment.
❌ -- Syntax Error -------------------------------------------------- file:///.../TestEffMultiple.flix
>> Illegal equality constraint.
126 | pub def composeAndReduceEq(eq: Composable.B[a][a], f: a -> Unit \ Composable.E[a], x: a): Bool \ Composable.E[a] with Composable[a], Eq[b] where Composable.B[a][a] ~ b =
^^^^^^^^^^^^^^^^^^^^^^
Equality constraints must have the form: `Assoc[var] ~ Type`.
There was a problem hiding this comment.
Ah, that's a trickier problem. We can't currently do a constraint Eq[X[a]] if X is abstract. It's a design question. See https://hackage.haskell.org/package/base-4.15.0.0/docs/Data-Functor-Classes.html#t:Eq1
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Related to #7424