Unify the two DSLs for RISE into a single one #76
Conversation
michel-steuwer
requested review from
Bastacyclop,
bastian-koepcke and
fedepiz
| def untypedTopLevel[T <: Expr](d: ToBeTyped[T]): ToBeTyped[TopLevel] = | ||
| toBeTyped(topLevel(toExpr(d))) | ||
|
|
||
| def eraseTypeFromExpr[T <: Expr](e: T): T = |
There was a problem hiding this comment.
maybe this should be private, or contain the word unsafe?
| val constraints = mutable.ArrayBuffer[Constraint]() | ||
| val (typed_e, ftvSubs) = constrainTypes(e, constraints, mutable.Map()) | ||
| val solution = unfreeze(ftvSubs, Constraint.solve(constraints.toSeq, Seq())(explDep)) | ||
| traversal.DepthFirstLocalResult(typed_e, Visitor(solution)) |
There was a problem hiding this comment.
will this DSL inference perform something like printTypeAndTypeHoles?
There was a problem hiding this comment.
does this DSL enforce unique names for type inference and DPIA?
There was a problem hiding this comment.
I do not know the relationship to printTypeAndTypeHoles (neither do I understand what is done there).
We are not enforcing unique names in the type inference process.
Substitution is no longer relying on unique names.
There was a problem hiding this comment.
printTypeAndTypeHoles will handle debug primitives:
- print the types of the
printTypeprimitives - print the types of the
typeHoleprimitives, throwing an error if a type hole is found (because a type hole makes the expression incomplete)
I think that we should add this to the new DSL type inference (while avoiding excessive prints), or alternatively move this code to fromRise on the transition to DPIA.
There was a problem hiding this comment.
About unique names, I think that we still require unique names on the DPIA side, so we might want to move the enforce to fromRise if the type inference does not require it anymore.
| val bnfExpr = normalize(ev).apply(betaReduction)(expr).get | ||
| // TODO: consider if we can remove this going forward | ||
| val exprWithUniqueNames = uniqueNames.enforce(expr) | ||
| val bnfExpr = normalize(ev).apply(betaReduction)(exprWithUniqueNames).get |
There was a problem hiding this comment.
beta reduction can break unique names ((fun x. x x) (fun y. y) --> (fun y. y) (fun y. y)), maybe we should enforce unique names after normalization.
This should be revisited in a separate PR.
…aints for one long running test.
|
I have delayed the implementation of the enforcement of unique names and suggest we accept this PR without it and I will look at this in a separate PR. I hope that's fine with you @Bastacyclop. |
This PR removes the DSL that helped to construct untyped expressions for which the type has to be inferred explicitly with a call to
infer.The only remaining DSL uses the
ToBeTypedclass to construct expressions for which the types are inferred automatically on conversion to theExprclass.This PR also introduces an import distinction in our interpretation of type annotations:
TypeAnnotations (writtene :: t) add a constraint that has to be resolved in type inferenceTypeAssertaions (writtene !: t) insist that the type inferred foremust be made compatible witht, that is, the constraint solving only goes one way, type variables intwill not be instantiated during constraint solving, only the once ine.t.The
TypeAsserations are used during rewriting, when we know already what the expected type of the replacement must be and we assert that the inferred type of the expression must be made compatible with the asserted type.By switching the DSLs this PR also rolls out syntax changes introduced in #70.