Simplify type variables #1263
Simplify type variables #1263
Conversation
There was a problem hiding this comment.
I started the review but I think that while I agree with points 1 and 3 in the description (removing mutability, using Dolmen variables), I don't think point 2 is a good idea.
Substitutions are well understood as maps from variables to terms and I think we should just use that; wrapping that in a module with a hard-to-understand interface (try_bind) seems to only bring unneeded complexity.
Can you update the PR to remove the Subst module and I'll finish my review (I think most of the comments were going to be about that module anyway)?
| val try_bind : tvar -> t -> subst -> subst | ||
| (** [try_bind tv ty sbt] tries to bind [tv] with [ty]. The function | ||
| succeeds if [tv] is not in the domain of [sbt] or the current | ||
| value of [tv] in [sbt] is equal to [ty]. | ||
|
|
||
| If the current value of [tv] is not compatible with [ty], raises | ||
| the exception {!exception TypeClash}. | ||
|
|
||
| If the previous value of [tv] in [sbt] is equal to [ty] for [equal], | ||
| the returned substitution is physically equal to [sbt]. *) | ||
|
|
There was a problem hiding this comment.
This could be made much simpler by simply exposing a function find that raises Not_found if the variable is not in the substitution.
There was a problem hiding this comment.
Actually, we do not need to expose this function because it is only used in the matching function of Ty. So we can use directly the find function.
During the last dev meeting, we agreed that this modification was not appropriate. As often, the mathematical way to present a data structure is not the best way to implement it. It is common to consider a substitution as a total map from as set |
|
Close in favor of #1267 |
This PR changes three thing:
types in the legacy typechecker.
Ty. I add two different functions in the new moduleSubstto update a substitution. The functionSubst.updateupdates a substitution without checking if it is compatible with a previous bind in the map. The functionSubst.try_bindupdates a substitution too but raisesTypeClashif a previous bind in the map is incompatible with the new value.Translatefor type variables but I think we can simplify this part too. I prefer doing it in a separate PR.