type-equations #63

Open
Olivier wants to merge 15 commits from type-equations into type-equations-master
Owner
No description provided.
Olivier added 11 commits 2023-01-23 10:08:16 +01:00
gasche reviewed 2023-01-23 12:35:15 +01:00
client/F.ml Outdated
@ -10,1 +10,3 @@
we must be able to display them as part of a type error message. *)
we must be able to display them as part of a type error message.
We use a restricted version of this system where a recursive cycle cannot
go through a universal quantifier. *)
Collaborator
  • Sauter une ligne avant, que ça fasse un paragraphe indépendant

  • "of this system" n'est pas ultra clair pour moi

  • Mentionner que c'est pour simplifier l'implémentation qu'on a mis cette restriction ?

  • Donner quelques exemples de types acceptés et rejetés: forall a. mu t. a -> t est accepté, mu t . forall a . (a -> t) est rejeté. Qu'en est-il de mu t . (forall a . a) -> t? D'après ton explication ça devrait être accepté, mais je soupçonne que le code le rejette, il y a une incohérence ici.

- Sauter une ligne avant, que ça fasse un paragraphe indépendant - "of this system" n'est pas ultra clair pour moi - Mentionner que c'est pour simplifier l'implémentation qu'on a mis cette restriction ? - Donner quelques exemples de types acceptés et rejetés: `forall a. mu t. a -> t` est accepté, `mu t . forall a . (a -> t)` est rejeté. Qu'en est-il de `mu t . (forall a . a) -> t`? D'après ton explication ça devrait être accepté, mais je soupçonne que le code le rejette, il y a une incohérence ici.
Olivier marked this conversation as resolved
client/F.ml Outdated
@ -57,0 +64,4 @@
[Use] is a construct that "opens" a type equality. That is, it allows to
reason in a context a context where two types are assumed to be equals.
It is supposed to be used with a [Refl] as a left-hand side :
Collaborator

Euh, non ? Les cas intéressants sont ceux où le terme de type TyEq(ty1, ty2) n'est pas un Refl mais un paramètre venant de l'extérieur / d'une structure de donnée. use (Refl ty) in t est toujours équivalent à t, puisqu'on introduit seulement l'égalité triviale ty = ty dans le contexte.

Euh, non ? Les cas intéressants sont ceux où le terme de type `TyEq(ty1, ty2)` n'est pas un `Refl` mais un paramètre venant de l'extérieur / d'une structure de donnée. `use (Refl ty) in t` est toujours équivalent à `t`, puisqu'on introduit seulement l'égalité triviale `ty = ty` dans le contexte.
Olivier marked this conversation as resolved
@ -211,1 +211,4 @@
str "The variable %s is unbound." x
| UnboundTypeVariable x ->
str "Scope error." ++
str "The variable %d is unbound." x
Collaborator

The type variable

`The type variable`
Olivier marked this conversation as resolved
@ -72,0 +80,4 @@
[store] and [tyvars] *)
type consistency =
| Consistent of store * tyvars
| Inconsistent
Collaborator

Le nommage ici est bizarre: pourquoi une information de cohérence (consistency) contient-elle un store ?

Contre-proposition:

type uf_store = structure option UF.store
type uf_tyvars = structure option UF.elem

type equation_env =
  | Equations of { store: uf_store; tyvars: uf_tyvars }
  | Inconsistent
Le nommage ici est bizarre: pourquoi une information de cohérence (`consistency`) contient-elle un store ? Contre-proposition: ```ocaml type uf_store = structure option UF.store type uf_tyvars = structure option UF.elem type equation_env = | Equations of { store: uf_store; tyvars: uf_tyvars } | Inconsistent ```
Olivier marked this conversation as resolved
@ -200,3 +219,2 @@
(* This function assumes that no occurence of forall quantification
appear under a mu-type. *)
(* This function assumes no universal quantification inside a μ-type.
Collaborator

Pourquoi ? Parce qu'on ne sait pas tester l'équivalence entre types simplement dans ce cas.

Pourquoi ? Parce qu'on ne sait pas tester l'équivalence entre types simplement dans ce cas.
Olivier marked this conversation as resolved
@ -272,0 +296,4 @@
- decompose an equality assumption
- perform an equality check
Since these two operations can be break down into similar parts, we
factorize the code, by passing a [mode] argument to the functions. *)
Collaborator

Je pense qu'on pourrait reformuler cette partie ensemble à notre prochaine discussion.

Je pense qu'on pourrait reformuler cette partie ensemble à notre prochaine discussion.
Olivier marked this conversation as resolved
@ -315,2 +351,2 @@
let (--) ty1 ty2 env : unit =
if not (equal Check env ty1 ty2) then
(* Re-package the type equality test as a type equality check. *)
let equal env ty1 ty2 : unit =
Collaborator

check_equal? enforce_equal? Pour moi une fonction equal renvoie un bool.

`check_equal`? `enforce_equal`? Pour moi une fonction `equal` renvoie un `bool`.
Olivier marked this conversation as resolved
@ -402,0 +442,4 @@
typeof { env with uf_state = Inconsistent } u
| ty ->
raise (TypeError (NotAnEqual ty))
end
Collaborator

Cette logique serait plus claire avec une fonction auxiliare

val add_equation : equation_env -> ty -> ty -> equation_env

(j'utilise le nom equation_env que j'ai proposé plutôt que consistency actuellement, mais c'est la même chose.)

Cette logique serait plus claire avec une fonction auxiliare ```ocaml val add_equation : equation_env -> ty -> ty -> equation_env ``` (j'utilise le nom `equation_env` que j'ai proposé plutôt que `consistency` actuellement, mais c'est la même chose.)
Olivier marked this conversation as resolved
@ -4,0 +6,4 @@
let check
(env : F.nominal_datatype_env) (t : F.nominal_term)
(on_error : FTypeChecker.type_error -> unit)
(on_ok : unit -> unit)
Collaborator

En fait, est-ce que le code ne serait pas plus simple et plus clair si on changeait cette fonction pour renvoyer un (debruijn_type, type_error) result ? Ou éventuellement (unit, type_error) result si on sait qu'on n'utilise jamais le type calculé.

En fait, est-ce que le code ne serait pas plus simple et plus clair si on changeait cette fonction pour renvoyer un `(debruijn_type, type_error) result` ? Ou éventuellement `(unit, type_error) result` si on sait qu'on n'utilise jamais le type calculé.
Olivier marked this conversation as resolved
Olivier added 5 commits 2023-01-24 14:13:52 +01:00
Olivier added 1 commit 2023-01-24 14:49:00 +01:00
gasche reviewed 2023-01-24 15:23:00 +01:00
client/F.ml Outdated
@ -12,0 +13,4 @@
(* Types mixing ∀ and μ are difficult to compare in general. To simplify
equality checking, we do not permit recursive cycles through universal
quantifiers, that is, we don't allow under μ.
Collaborator

"we do not permit recursive cycles through universal
quantifiers" and "we don't allow ∀ under μ" (do not) ne sont pas équivalents. La première version accepte le troisième exemple, la deuxième (qu'on implémente) le rejette.

"we do not permit recursive cycles through universal quantifiers" and "we don't allow ∀ under μ" (do not) ne sont pas équivalents. La première version accepte le troisième exemple, la deuxième (qu'on implémente) le rejette.
Olivier marked this conversation as resolved
client/F.ml Outdated
@ -57,0 +78,4 @@
... (* here ty1 and ty2 are assumed to be equal *)
Doing this might introduce inconsistent assumptions about types (this can
occur for example inside a pattern matching). That is why we introduce
Collaborator

donner l'exemple int = bool ?

donner l'exemple `int = bool` ?
client/F.ml Outdated
@ -57,0 +80,4 @@
Doing this might introduce inconsistent assumptions about types (this can
occur for example inside a pattern matching). That is why we introduce
a construct [Absurd], that can be used as a placeholder in pieces of code
where it happens and that are thus unreachable. *)
Collaborator

"where it happens" => "with inconsistent equations in the environment"

"where it happens" => "with inconsistent equations in the environment"
Olivier marked this conversation as resolved
@ -216,2 +219,3 @@
str "Type error." ++
str "The context is not absurd"
str "The typing context was expected to be inconsistent but is not." ++
str "This means that two types were assumed to be different but are not."
Collaborator

The type equations in the typing environment are not contradictory.

The type equations in the typing environment are not contradictory.
Olivier marked this conversation as resolved
@ -81,3 +90,1 @@
(* Is set to false when an inconsistent equation is introduced in the
environment. It is useful while typechecking pattern-matching. *)
consistent: bool;
(* We keep trace of wheter or not the typing equations is consistent *)
Collaborator

whether

whether
Olivier marked this conversation as resolved
@ -89,3 +97,1 @@
store = UF.new_store();
tyvars = [];
consistent = true;
equations_env = Equations { store = UF.new_store() ; tyvars = [] };
Collaborator

"equations" here would work as well (env.equations), but equations_env is okay.

"equations" here would work as well (`env.equations`), but `equations_env` is okay.
Olivier marked this conversation as resolved
@ -203,0 +220,4 @@
(* This function assumes no universal quantification inside a μ-type, because
it would be difficult to check type equality otherwise. That is why we need
a boolean [inside_mu] during the traversal of the type to remember wether
or not we are under a μ-quantification *)
Collaborator

The boolean [inside_mu] tracks whether we are already under a μ quantifier.

The boolean [inside_mu] tracks whether we are already under a μ quantifier.
Olivier marked this conversation as resolved
@ -272,0 +297,4 @@
- decompose an equality assumption
- perform an equality check
Since these two operations can be break down into similar parts, we
factorize the code, by passing a [mode] argument to the functions. *)
Collaborator

We need two operations on equalities between types:

  • add an equality to the equations in the environment
  • check if a given equality holds modulo the equations in the environment

Both operations can be described as first decomposing a given equality "ty1 = ty2"
into "simple equalities" between a rigid variable and a type. In fact, the union-find data structure
that we use to represent an environment of equations store exactly those simple equlities.
Then:

  • to add an equality, we modify our environment by unifying the type variables with the equated type
  • to check an equality, we check that the simple equalities are already valid in the equations of the environment, and fail otherwise

The decomposition process does not produce simple equalities if the provided equality is absurd ("intint = intbool"). Then:

  • if we are adding this equality to the environment, we record that the environment is now Inconsistent
  • if we are checking the equality (in a consistent environment), we fail

The functions below implement a unification procedure that implements both these operations, depending on a [mode] parameter:

  • in [Input] mode, they add an equality to the environment
  • in [Check] mode, they check that the equality holds modulo the equations in the environment
We need two operations on equalities between types: - add an equality to the equations in the environment - check if a given equality holds modulo the equations in the environment Both operations can be described as first decomposing a given equality "ty1 = ty2" into "simple equalities" between a rigid variable and a type. In fact, the union-find data structure that we use to represent an environment of equations store exactly those simple equlities. Then: - to add an equality, we modify our environment by unifying the type variables with the equated type - to check an equality, we check that the simple equalities are already valid in the equations of the environment, and fail otherwise The decomposition process does not produce simple equalities if the provided equality is absurd ("int*int = int*bool"). Then: - if we are adding this equality to the environment, we record that the environment is now Inconsistent - if we are checking the equality (in a consistent environment), we fail The functions below implement a unification procedure that implements both these operations, depending on a [mode] parameter: - in [Input] mode, they add an equality to the environment - in [Check] mode, they check that the equality holds modulo the equations in the environment
Olivier marked this conversation as resolved
@ -313,1 +348,3 @@
(* Re-package the type equality test as a type equality check. *)
(* Re-package the type equality assumption as a type consistency check. *)
let consistent env ty1 ty2 : bool =
unify_types Input env ty1 ty2
Collaborator

Je propose de ne pas renvoyer un booléen mais un nouvel environment -- en fait ça renvient à inliner ce code dans add_equation.

Je propose de ne pas renvoyer un booléen mais un nouvel environment -- en fait ça renvient à inliner ce code dans `add_equation`.
Olivier marked this conversation as resolved
@ -396,0 +439,4 @@
| Equations { store ; tyvars } ->
let store_copy = UF.copy store in
let equations_env = Equations { store = store_copy; tyvars } in
let env = { env with equations_env } in
Collaborator

on pourrait avoir un fonction copy_env : env -> env

on pourrait avoir un fonction `copy_env : env -> env`
Olivier marked this conversation as resolved
Olivier added 6 commits 2023-01-24 16:14:44 +01:00
Olivier force-pushed type-equations from 84491c2846 to a6b17c8d94 2023-01-24 16:41:42 +01:00 Compare
Olivier force-pushed type-equations from a6b17c8d94 to 934fb82b15 2023-01-25 11:31:26 +01:00 Compare
This pull request has changes conflicting with the target branch.
  • client/FPrinter.ml
  • client/FTypeChecker.ml
  • client/test/CheckF.ml
  • client/test/TestF.ml
You can also view command line instructions.

Step 1:

From your project repository, check out a new branch and test the changes.
git checkout -b type-equations type-equations-master
git pull origin type-equations

Step 2:

Merge the changes and update on Gitea.
git checkout type-equations-master
git merge --no-ff type-equations
git push origin type-equations-master
Sign in to join this conversation.
No reviewers
No Label
No Milestone
No Assignees
2 Participants
Notifications
Due Date
The due date is invalid or out of range. Please use the format 'yyyy-mm-dd'.

No due date set.

Dependencies

No dependencies set.

Reference: Olivier/inferno-experimental#63
No description provided.