cduce issueshttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues2024-03-20T00:24:15+01:00https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/37Unsoundness in polymorphic subtying2024-03-20T00:24:15+01:00Kim NguyễnUnsoundness in polymorphic subtyingCDuce says that the following simingly equal types are not equivalent (while they should be). Computing their differences yields a bogus type `[ Empty]` (which should never be printed, since it is empty).
The problem is twofold:
- I thi...CDuce says that the following simingly equal types are not equivalent (while they should be). Computing their differences yields a bogus type `[ Empty]` (which should never be printed, since it is empty).
The problem is twofold:
- I think the pretty-printer is wrong and `[Empty]` is not displaying some variables that should be there (it appended before)
- If the type really are equivalent (and not wrongly displayed as equivalent) then a bug lurks in the subtyping.
```
SIMPLIFY ERROR
[ [ ('7M_9 & '8M_10) '7M_9* ] '7M_9* ]
[ [ ('7M_9 & '8M_10) '7M_9* ] '7M_9* ]
Initial type:
=========
<types = [ [ ('7M_9 & '8M_10) '7M_9* ] '7M_9* ]
ints(F)
atoms(F)
chars(F)
abstract(F)
times((X458,X46)(+(X919,X46)(F,F,-(X960,X958)(T,F,F)),F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X458=<types = Any \ [ ]
ints(T)
atoms(Cofinite[(->Finite[[ ]])])
chars(T)
abstract(T)
times(T)
xml(T)
record(T)
arrow(T)
absent=false>
X958=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X959,X958)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X46=ANY
X919=<types = Any \ (Any \ '7M_9 | '8M_10,Any)
ints(T)
atoms(T)
chars(T)
abstract(T)
times((X910,X46)(F,F,T))
xml(T)
record(T)
arrow(T)
absent=false>
X960=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X961,X960)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X910=<types = Any \ '7M_9 | '8M_10
ints(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
atoms(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
chars(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
abstract(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
times(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
xml(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
record(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
arrow(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
absent=false>
X961=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
X959=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>Simplified type:
=========
<types = [ [ ('7M_9 & '8M_10) '7M_9* ] '7M_9* ]
ints(F)
atoms(F)
chars(F)
abstract(F)
times((X1148,X1147)(F,F,-(X1152,X1150)(+(X1154,X1147)(T,F,F),F,F)))
xml(F)
record(F)
arrow(F)
absent=false>
X1154=<types = Any \ [ ]
ints(T)
atoms(Cofinite[(->Finite[[ ]])])
chars(T)
abstract(T)
times(T)
xml(T)
record(T)
arrow(T)
absent=false>
X1148=<types = Any \ (Any \ '7M_9 | '8M_10,Any)
ints(T)
atoms(T)
chars(T)
abstract(T)
times((X1149,X1147)(F,F,T))
xml(T)
record(T)
arrow(T)
absent=false>
X1147=ANY
X1152=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X1153,X1152)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X1150=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X1151,X1150)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X1149=<types = Any \ '7M_9 | '8M_10
ints(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
atoms(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
chars(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
abstract(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
times(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
xml(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
record(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
arrow(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
absent=false>
X1153=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
X1151=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
========
======== Simp\Initial (false):
@<types = [ Empty ]
ints(F)
atoms(F)
chars(F)
abstract(F)
times((X458,X46)(+(X919,X46)(+(X1148,X1147)(F,F,
-(X1152,X1150)(+(X1154,X1147)
(T,F,F),
F,F)),
F,
-(X960,X958)(F,F,
-(X1148,X1147)(F,F,
-(X1152,X1150)
(+(X1154,X1147)
(T,F,F),
F,F)))),
F,
-(X1148,X1147)(F,F,
-(X1152,X1150)(+(X1154,X1147)(T,F,F),F,F))))
xml(F)
record(F)
arrow(F)
absent=false>
X1154=<types = Any \ [ ]
ints(T)
atoms(Cofinite[(->Finite[[ ]])])
chars(T)
abstract(T)
times(T)
xml(T)
record(T)
arrow(T)
absent=false>
X458=<types = Any \ [ ]
ints(T)
atoms(Cofinite[(->Finite[[ ]])])
chars(T)
abstract(T)
times(T)
xml(T)
record(T)
arrow(T)
absent=false>
X958=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X959,X958)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X46=ANY
X919=<types = Any \ (Any \ '7M_9 | '8M_10,Any)
ints(T)
atoms(T)
chars(T)
abstract(T)
times((X910,X46)(F,F,T))
xml(T)
record(T)
arrow(T)
absent=false>
X1148=<types = Any \ (Any \ '7M_9 | '8M_10,Any)
ints(T)
atoms(T)
chars(T)
abstract(T)
times((X1149,X1147)(F,F,T))
xml(T)
record(T)
arrow(T)
absent=false>
X1147=ANY
X1152=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X1153,X1152)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X1150=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X1151,X1150)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X960=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X961,X960)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X910=<types = Any \ '7M_9 | '8M_10
ints(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
atoms(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
chars(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
abstract(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
times(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
xml(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
record(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
arrow(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
absent=false>
X961=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
X1149=<types = Any \ '7M_9 | '8M_10
ints(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
atoms(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
chars(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
abstract(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
times(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
xml(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
record(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
arrow(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
absent=false>
X959=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
X1153=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
X1151=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
======== Initial\Simp (false):
@<types = [ Empty ]
ints(F)
atoms(F)
chars(F)
abstract(F)
times((X458,X46)(+(X919,X46)(F,F,
-(X960,X958)(+(X1148,X1147)(T,
=(X1152,X1150)
(F,
=(X1154,X1147)
(F,F,T),T),
F),
F,F)),
F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X1154=<types = Any \ [ ]
ints(T)
atoms(Cofinite[(->Finite[[ ]])])
chars(T)
abstract(T)
times(T)
xml(T)
record(T)
arrow(T)
absent=false>
X458=<types = Any \ [ ]
ints(T)
atoms(Cofinite[(->Finite[[ ]])])
chars(T)
abstract(T)
times(T)
xml(T)
record(T)
arrow(T)
absent=false>
X958=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X959,X958)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X46=ANY
X919=<types = Any \ (Any \ '7M_9 | '8M_10,Any)
ints(T)
atoms(T)
chars(T)
abstract(T)
times((X910,X46)(F,F,T))
xml(T)
record(T)
arrow(T)
absent=false>
X1148=<types = Any \ (Any \ '7M_9 | '8M_10,Any)
ints(T)
atoms(T)
chars(T)
abstract(T)
times((X1149,X1147)(F,F,T))
xml(T)
record(T)
arrow(T)
absent=false>
X1147=ANY
X1152=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X1153,X1152)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X1150=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X1151,X1150)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X960=<types = [ '7M_9* ]
ints(F)
atoms(Finite[(->Finite[[ ]])])
chars(F)
abstract(F)
times((X961,X960)(T,F,F))
xml(F)
record(F)
arrow(F)
absent=false>
X910=<types = Any \ '7M_9 | '8M_10
ints(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
atoms(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
chars(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
abstract(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
times(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
xml(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
record(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
arrow(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
absent=false>
X961=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
X1149=<types = Any \ '7M_9 | '8M_10
ints(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
atoms(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
chars(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
abstract(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
times(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
xml(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
record(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
arrow(VAR(9,7M,`user)(F,=VAR(10,8M,`user)(T,F,F),T))
absent=false>
X959=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
X1153=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
X1151=<types = '7M_9
ints(VAR(9,7M,`user)(T,F,F))
atoms(VAR(9,7M,`user)(T,F,F))
chars(VAR(9,7M,`user)(T,F,F))
abstract(VAR(9,7M,`user)(T,F,F))
times(VAR(9,7M,`user)(T,F,F))
xml(VAR(9,7M,`user)(T,F,F))
record(VAR(9,7M,`user)(T,F,F))
arrow(VAR(9,7M,`user)(T,F,F))
absent=false>
```Kim NguyễnKim Nguyễnhttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/33Issue with min_type and max_type2022-08-25T15:57:39+02:00Mickael LaurentIssue with min_type and max_typeThe description of the functions Type.Subst.min_type and Type.Subst.max_type in the doc is wrong:
the largest subtype of any instance of t is NOT t where all positive occurrences of variables are replaced by 𝟘 and all negative occurrence...The description of the functions Type.Subst.min_type and Type.Subst.max_type in the doc is wrong:
the largest subtype of any instance of t is NOT t where all positive occurrences of variables are replaced by 𝟘 and all negative occurrences of variables not in vars are replaced by 𝟙.
Counterexample:
`t = (Any->Any) & 'a | (Int->Int) & ~'a`
min(t) should be `(Any->Any)&(Int->Int)`, but replacing the occurences of 'a as specified would give Empty,
which is a subtype of any instance of t but not the largest.
Moreover, the result of this computation is not preserved by semantic equivalence, as for any `'a` we have `(Int->Int) = (Int->Int) & 'a | (Int->Int) & ~'a` but `min(Int->Int) = Int->Int` and `min((Int->Int) & 'a | (Int->Int) & ~'a) = Empty`. Also, I am not sure Cduce would always simplify the type `(Int->Int) & 'a | (Int->Int) & ~'a` into `(Int->Int)` as it does not simplify the DNF of functions.
The cases where the functions min_type and max_type are not correct is when a variable appears in both a negative and positive occurence, because then the operation of substituting one of the occurence by something and the other by something else is not preserved by semantic equivalence.
I understand that one of the usecase of this function is to implement the min and max for dynamic types, but as dynamic type variables should always be unique (a given dynamic type variable should not appear twice in a type), the function clean_type should be enough to implement it (as a given dynamic type variable can only be positive or negative but not both). If a dynamic type variable "semantically" appears in both covariant and contravariant positions, it is invalid and thus the fact that clean_type will do nothing is not an issue (assuming that Cduce will simplify trivial partitions of the form `t & 'a | t & ~'a` in order to only keep occurences of variables that have a semantic impact, which I don't think is always true when t is a function for instance).
My suggestion is to remove the min_type and max_type functions as the cases where it is correct (when no variable is both in covariant and contravariant position) can easily be handled with clean_type.https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/26Weak polymorphism is not unified nor propagated when used in a function2022-02-01T17:00:39+01:00MattiasWeak polymorphism is not unified nor propagated when used in a functionSome examples here:
```ocaml
# let r = ref ([ 'a* ]) [];;
val r : { get=[ ] -> [ '_weak0* ] set=[ '_weak0* ] -> [ ] } = { get=<fun>
# let f (x : Int) : Int = r := [ x ]; x + 1;;
val f : Int -> Int = <fun>
# r;;
- : { get=[ ] -> [ '_...Some examples here:
```ocaml
# let r = ref ([ 'a* ]) [];;
val r : { get=[ ] -> [ '_weak0* ] set=[ '_weak0* ] -> [ ] } = { get=<fun>
# let f (x : Int) : Int = r := [ x ]; x + 1;;
val f : Int -> Int = <fun>
# r;;
- : { get=[ ] -> [ '_weak0* ] set=[ '_weak0* ] -> [ ] } = { get=<fun>
set=<fun> }
```
```ocaml
# let g (x : 'a) : 'a = r := [ x ]; x;;
val g : 'a -> 'a = <fun>
# g 3;;
- : 3 = 3
# g;;
- : 'a -> 'a = <fun>
# r;;
- : { get=[ ] -> [ '_weak0* ] set=[ '_weak0* ] -> [ ] } = { get=<fun>
set=<fun> }
```Kim NguyễnKim Nguyễnhttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/25Issue in apply that makes it not monotone2022-01-30T14:35:33+01:00Mickael LaurentIssue in apply that makes it not monotoneWhen intersecting an arrow type whose dnf contain several conjunctions,
if this intersection makes one of the conjunctions empty, it will not be simplified in the DNF.
Then, using the operator apply on this arrow type will consider the ...When intersecting an arrow type whose dnf contain several conjunctions,
if this intersection makes one of the conjunctions empty, it will not be simplified in the DNF.
Then, using the operator apply on this arrow type will consider the positive part of this empty conjunction and thus it will not yield the expected type but a larger one.
This can be reproduced with the following code:
```ocaml
module CD = Cduce_types
let cup t1 t2 = CD.Types.cup t1 t2
let cap t1 t2 = CD.Types.cap t1 t2
let diff = CD.Types.diff
let cons = CD.Types.cons
let mk_arrow = CD.Types.arrow
let true_typ = CD.Builtin_defs.true_type
let false_typ = CD.Builtin_defs.false_type
let bool_typ = cup true_typ false_typ
let int_typ = CD.Types.Int.any
let any = CD.Types.any
let empty = CD.Types.empty
let any_node = cons any
let empty_node = cons empty
let subtype = CD.Types.subtype
let pp_typ = CD.Types.Print.print_noname
let apply t args =
let t = CD.Types.Arrow.get t in
CD.Types.Arrow.apply t args
let arrow_any = CD.Types.Function.any
let domain t =
if subtype t arrow_any then
let t = CD.Types.Arrow.get t in
CD.Types.Arrow.domain t
else empty
let _ =
let simple_arrow = mk_arrow (cons int_typ) (cons int_typ) in
let test = simple_arrow in
let test = cup test (mk_arrow (cons bool_typ) any_node) in
let test = diff test (mk_arrow any_node any_node) in
let test = cap test (mk_arrow (cons (diff any bool_typ)) any_node) in
Format.printf "%a@." pp_typ test ;
Format.printf "Subtype of %a ? %b@." pp_typ simple_arrow (subtype test simple_arrow) ;
Format.printf "But when we apply an Int to it: %a@." pp_typ (apply test (domain simple_arrow)) ;
```
It has been tested on the branches dune-switch and polymorphic.Kim NguyễnKim Nguyễnhttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/18Unsoundness with testing of function types2021-05-02T10:25:08+02:00Tommaso PetruccianiUnsoundness with testing of function typesThis code
(fun ((Int -> Int) -> `true; (Any \ (Int -> Int)) -> `false)
| ((Int -> Int) \ (Bool -> Bool)) -> `true
| (Int -> Int) & (Bool -> Bool) -> `true
| _ -> `false)
(fun (x: Int): Int = x + 1)
breaks type pre...This code
(fun ((Int -> Int) -> `true; (Any \ (Int -> Int)) -> `false)
| ((Int -> Int) \ (Bool -> Bool)) -> `true
| (Int -> Int) & (Bool -> Bool) -> `true
| _ -> `false)
(fun (x: Int): Int = x + 1)
breaks type preservation (in the cduce-next branch), producing
- : `true = false
The first function is well-typed; in particular, when the argument has type `Int -> Int`, the result must be `true` since either of the first two branches must apply (together, they cover `Int -> Int` entirely). The application is well-typed as well, but it reduces to the third branch (which is statically predicted to be unused) because the second function can be assigned neither type `(Int -> Int) \ (Bool -> Bool)` nor type `(Int -> Int) & (Bool -> Bool)`.
This behaviour actually seems consistent with that described in the formalization (POPL '14 and '15), but it's unsound. When type tests are performed at runtime functions should probably be given negations of arrow types to ensure soundness. I'm not sure how this interacts with polymorphism though.https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/17Unsoundness with record typing2021-05-02T10:41:43+02:00Tommaso PetruccianiUnsoundness with record typingFunctions on records can be given unsound types as in the following:
# let f = fun ({..} -> 'a) x -> x;;
val f : Record -> 'a = <fun>
# f {};;
- : 'a = { }
It seems that this `'a` cannot be instantiated:
# (f {}) + 1;;
Characte...Functions on records can be given unsound types as in the following:
# let f = fun ({..} -> 'a) x -> x;;
val f : Record -> 'a = <fun>
# f {};;
- : 'a = { }
It seems that this `'a` cannot be instantiated:
# (f {}) + 1;;
Characters 1-5:
This expression should have type:
!float | { .. } | Int
but its inferred type is:
'a
which is not a subtype, as shown by the sample:
Atom & 'a
However, here it becomes unsound:
# f (f {});;
- : Empty = { }
Typing of field removal is also unsound:
# let g = fun ({a=Int;b=Bool;..}&'a -> {b=Bool;..}&'a) x -> x\a;;
val g : { a=Int b=Bool .. } & 'a -> { b=Bool .. } & 'a = <fun>
# g {a=2;b=`true};;
- : { a=2 b=`true } = { b=true }
# (g {a=2;b=`true}).a;;
- : 2 = true
# (g {a=2;b=`true}).b;;
- : `true = true
# (g {a=2;b=`true}).a + 2;;
File "runtime/value.ml", line 873, characters 9-15: Assertion failedKim NguyễnKim Nguyễnhttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/13Tallying: failure in recursive calls inside merge make the whole merge fail2021-05-02T15:32:53+02:00Tommaso PetruccianiTallying: failure in recursive calls inside merge make the whole merge failCurrently `Type_tallying.merge` raises an exception if a constraint set is unsolvable. This exception is handled by `Type_tallying.type_tallying` but not by `merge` itself. Thus, if a recursive call inside `merge` fails, the whole call f...Currently `Type_tallying.merge` raises an exception if a constraint set is unsolvable. This exception is handled by `Type_tallying.type_tallying` but not by `merge` itself. Thus, if a recursive call inside `merge` fails, the whole call fails.
In particular, tallying fails on the constraint set
```
'a <= 'b -> 'c
1 <= 'b
'a -> 'c <= ('f -> 'f) -> 'e
```
(which admits a solution 'a := (1 -> 1), other variables := 1).
Test with
```
debug tallying [] ( 'a , ( 1 , ('a -> 'c) ) ) ( ('b -> 'c), ( 'b , (('f -> 'f) -> 1) ) );;
```
(here tallying finds only the solution `'a := Empty` and not the other one).
Normalization generates two constraints, one for `'a := Empty`, the other
```
{ 'f -> 'f <= 'a <= 'b -> 'c, 1 <= 'b <= Any, Empty <= 'c <= 1 }
```
which is not solved correctly. In `merge`, the contraint
`'f -> 'f <= 'b -> 'c` is generated and normalised into
```
{ { Empty <= 'b <= 'f, 'f <= 'c <= Any }, { Empty <= 'b <= Empty } }
```
only the first of which is solvable (since `1 <= 'b`, `'b <= Empty` is impossible). The case `'b <= Empty` is considered first and `merge` fails completely instead of considering the other case.
Replacing line 605
```
let m1' = merge delta cache m1 in
```
with
```
let m1' = try merge delta cache m1 with UnSatConstr _ -> ConstrSet.unsat in
```
solves this. I'm not sure if it breaks anything else, but it seems to be what the specification of tallying says (the recursive calls are in union with each other, so empty sets are ignored).Kim NguyễnKim Nguyễnhttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/12Solving type equation with recursive types for a variable 'a does not work wh...2017-10-16T08:48:07+02:00Kim NguyễnSolving type equation with recursive types for a variable 'a does not work when 'a occurs below a union/intersection/negationThe problem is in decompose and solve_rectype in Types. The Positive module giving the least fix point solution of a system of equation (aka Courcelle) does not work when variable occurs below type connective.
See for instance:
```
...The problem is in decompose and solve_rectype in Types. The Positive module giving the least fix point solution of a system of equation (aka Courcelle) does not work when variable occurs below type connective.
See for instance:
```
debug tallying [] [ (Int, 'a),'b ; 'b, 'a ] ;;
```
Kim NguyễnKim Nguyễnhttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/10Loop/errors on tallying2021-05-02T14:34:55+02:00Kim NguyễnLoop/errors on tallyingThis loops
<pre>
let x : (Int -> Int) & ('b -> 'b) & (('a -> 'a) -> ('a -> 'a)) = fun (x : 'd ) : ('d) = x : ('d) ;;
</pre>
This gives the wrong result
<pre>
# let x : (('a -> 'a) -> ('a -> 'a)) & (Int -> Int) & ('d -> 'd) = fun (x : '...This loops
<pre>
let x : (Int -> Int) & ('b -> 'b) & (('a -> 'a) -> ('a -> 'a)) = fun (x : 'd ) : ('d) = x : ('d) ;;
</pre>
This gives the wrong result
<pre>
# let x : (('a -> 'a) -> ('a -> 'a)) & (Int -> Int) & ('d -> 'd) = fun (x : 'd ) : ('d) = x : ('d) ;;
This expression should have type:
'd -> 'd
but its inferred type is:
(('a -> 'a) -> 'a -> 'a) & (Int -> Int) & ('d -> 'd)
</pre>
while each separate intersection works:
<pre>
# let x : (('a -> 'a) -> ('a -> 'a)) & (Int -> Int) = fun (x : 'd ) : ('d) = x : ('d) ;;
val x : (Int -> Int) & (('a -> 'a) -> 'a -> 'a) = <fun>
# let x : ('d -> 'd) = fun (x : 'd ) : ('d) = x : ('d) ;;
val x : 'd -> 'd = <fun>
</pre>https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/8Type error in patricia trees2021-05-02T14:55:48+02:00Kim NguyễnType error in patricia treesWith the current commit 25b127810a48fae75a795ca3bfc9fe7f388a6c11 patricia trees attached (see also [tests/poly/patricia.cd] in the distribution) [merge] function does not type. The error is
```
File "tests/poly/patricia.cd", line 69, cha...With the current commit 25b127810a48fae75a795ca3bfc9fe7f388a6c11 patricia trees attached (see also [tests/poly/patricia.cd] in the distribution) [merge] function does not type. The error is
```
File "tests/poly/patricia.cd", line 69, characters 31-43:
This expression should have type:
Empty
but its inferred type is:
'a
which is not a subtype, as shown by the sample:
'a & Int
```
The line at issue is
```
| (<leaf key=k>x , t) -> insert c k x t
```
And the error message states that at the position of x was wating somethig of an empty type. Let us show why. First notice that
```
insert : ('a -> 'a -> 'a) -> Caml_int -> 'a -> Dict -> Leaf|Branch
```
since we have the following declaration
```
let insert (c: 'a -> 'a -> 'a) (k: Caml_int) (x: 'a) (t: Dict): Leaf|Branch
```
First of all let us replace the line 69 with the following one:
```
| (<leaf key=k>x , t) -> insert
```
we **correctly** obtain the following error:
```
File "tests/poly/patricia.cd", line 69, characters 31-37:
This expression should have type:
Branch | Leaf
but its inferred type is:
('_a_0 -> '_a_0 -> '_a_0) -> Caml_int -> '_a_0 -> [ ] | <brch bit=Caml_int
pre=Caml_int>X1 | <leaf key=Caml_int>'_a_0 -> X2 where
X1 = [ X2 X2 ] and
X2 = <brch bit=Caml_int pre=Caml_int>X1 | <leaf key=Caml_int>'_a_0
which is not a subtype, as shown by the sample:
('_a_0 -> '_a_0 -> '_a_0) -> Caml_int -> '_a_0 -> [ ] | <brch bit=Caml_int
pre=Caml_int>X1 | <leaf key=Caml_int>'_a_0 -> X2 where
X1 = [ X2 X2 ] and
X2 = <brch bit=Caml_int pre=Caml_int>X1 | <leaf key=Caml_int>'_a_0
```
Notice two things: the system expects as result of the matching something of type ``Leaf|Branch`` (perfect!) and the type deduced for @insert@ is exactly the original type where ``'a`` has been renamed into a fresh variable. If now I use for this line the following definition
```
| (<leaf key=k>x , t) -> insert c
```
I expect that the fresh variable ``'_a_0`` is unified with ``'a`` of the type of ``c``, and thus that this expression has type ``Caml_int -> 'a -> Dict -> Leaf|Branch``. Instead we obtain:
```
File "tests/poly/patricia.cd", line 69, characters 31-39:
This expression should have type:
Branch | Leaf
but its inferred type is:
Caml_int -> Arrow
which is not a subtype, as shown by the sample:
Caml_int -> Arrow
```
So what did happen? Well the fresh variable ``'_a_0`` was **WRONGLY** substituted by Empty instead of by ``'a``. And therefore the deduced type is
```
Caml_int -> Empty -> Dict -> Leaf|Branch
```
(i.e. ``Caml_int -> Arrow``). This explain why feeding two more arguments to it we obtain the error message that the function was expecting something of type Empty. Indeed with
```
| (<leaf key=k>x , t) -> insert c k x
```
we obtain
```
File "tests/poly/patricia.cd", line 69, characters 31-43:
This expression should have type:
Empty
but its inferred type is:
'a
which is not a subtype, as shown by the sample:
'a & Int
```Kim NguyễnKim Nguyễnhttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/7Typechecking should only use squaresubtype when checking a result type agains...2021-05-02T14:53:42+02:00Kim NguyễnTypechecking should only use squaresubtype when checking a result type against an expected constraintThe typechecking function as the following signature:
```
type_check loc env constr e
```
where ``loc`` is a location, env is the environment, ``constr`` is an expected type and ``e`` is the expression to type-check. It returns an expres...The typechecking function as the following signature:
```
type_check loc env constr e
```
where ``loc`` is a location, env is the environment, ``constr`` is an expected type and ``e`` is the expression to type-check. It returns an expression ``e'`` (where some expressions may have been modified, e.g. branch of patterns specialized, unneeded cast removed etc.) and an output type ``t``. The last thing it often does before returning is:
```
verify loc t constr
```
which checks that indeed, ``t`` is a subtype of the expected constraint ``constr`` (for instance, when typing the body of a function, the constraint is the expected result type of the function). ``verify`` uses plain subtyping which is wrong. It should:
use ``squaresubtype_delta`` to check if there exists substitutions s1,...,sn such that t < constr
return not, t but t{s1} & ... & t{sn}
Note that because typechecking is half half between the old monomorphic code and the new polymorphic code (buggy) we end up with either weird type error or even unsound and clearly ill-typed code that compiles:
```
let f (<bar>['a] -> <foo>['a]) <bar>[ x ] -> <foo>[x]
;;
let f (<bar>['a] -> <foo>['a]) <bar>[ y ] -> <foo>[ y]
in
let apply (x : 'b) : 'b =
f x
;;
```
the body of apply is clearly wrong yet it compiles with the current master.
We need to thoroughly review the code of ``type_check`` (and other functions) to check for the following:
+ check everywhere there is an instance of ``Types.subtype`` to see whether ``Types.squaresubtype`` should be used instead.
+ properly review how the generalisation/freshening of type variables is doneKim NguyễnKim Nguyễnhttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/3Fix pretty printing of parentheses in types2021-05-02T14:51:06+02:00Kim NguyễnFix pretty printing of parentheses in typesSome types generate superfluous parentheses:
```
#print_type ('a | 'b ) \'c;;
(('a | 'b) \ ('c))
```
And some others are missing parenthses:
```
#print_type (Int -> Int) & (Bool -> Bool);;
Bool -> Bool & Int -> Int
# #print_type Bool -...Some types generate superfluous parentheses:
```
#print_type ('a | 'b ) \'c;;
(('a | 'b) \ ('c))
```
And some others are missing parenthses:
```
#print_type (Int -> Int) & (Bool -> Bool);;
Bool -> Bool & Int -> Int
# #print_type Bool -> Bool & Int -> Int;;
Bool -> Arrow
```
here we cannot paste the output of the toplevel.Kim NguyễnKim Nguyễn