cduce issueshttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues2021-10-08T17:49:17+02:00https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/2Determine the types of variables in matched expressions2021-10-08T17:49:17+02:00Kim NguyễnDetermine the types of variables in matched expressions```
fun (x : Int|Bool , y : Int | Bool) : Int | Bool =
match (x,y) with
| (Int,Bool) -> if y then x+3 else x +2
| _ -> x;;
```
does not type. In order to have it working we have to redefine the pattern as follows
```
fun (x : Int|Bool , y : Int | Bool) : Int | Bool =
match (x,y) with
| (Int,Bool)&(x,y) -> if y then x+3 else x +2
| _ -> x;;
```
Idea ... in order to refine the type of variables occuring in the MATCHED expression, then whenever this expression is ALSO A PATTERN rewrite it as follows:
```
match p with p1 -> e1 | ... | pn-> en
```
into
```
match p with p&p1 -> e1 | ... | p&pn-> en
```
Unfortunately this does not work when p and pi have a variable in common. We must find a smarter solution.```
fun (x : Int|Bool , y : Int | Bool) : Int | Bool =
match (x,y) with
| (Int,Bool) -> if y then x+3 else x +2
| _ -> x;;
```
does not type. In order to have it working we have to redefine the pattern as follows
```
fun (x : Int|Bool , y : Int | Bool) : Int | Bool =
match (x,y) with
| (Int,Bool)&(x,y) -> if y then x+3 else x +2
| _ -> x;;
```
Idea ... in order to refine the type of variables occuring in the MATCHED expression, then whenever this expression is ALSO A PATTERN rewrite it as follows:
```
match p with p1 -> e1 | ... | pn-> en
```
into
```
match p with p&p1 -> e1 | ... | p&pn-> en
```
Unfortunately this does not work when p and pi have a variable in common. We must find a smarter solution.https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/20Problem with parsing apostrophes2021-10-08T08:12:49+02:00Giuseppe CastagnaProblem with parsing apostrophes en utilisant la version polymorphe de CDuce:
```
opam pin add cduce-types
'git+https://gitlab.math.univ-paris-diderot.fr/cduce/cduce#polymorphic'
opam pin add cduce
'git+https://gitlab.math.univ-paris-diderot.fr/cduce/cduce#polymorphic'
```
on a un problème avec les apostrophes:
```
CDuce version 0.6.0-251-g97158a7b
# let nobreakspace = '\8239;' ;;
Characters 26-27:
Parsing error: Illegal character : '
```
Par contre ceci n'arrive pas avec la version monomorphe: en utilisant la version polymorphe de CDuce:
```
opam pin add cduce-types
'git+https://gitlab.math.univ-paris-diderot.fr/cduce/cduce#polymorphic'
opam pin add cduce
'git+https://gitlab.math.univ-paris-diderot.fr/cduce/cduce#polymorphic'
```
on a un problème avec les apostrophes:
```
CDuce version 0.6.0-251-g97158a7b
# let nobreakspace = '\8239;' ;;
Characters 26-27:
Parsing error: Illegal character : '
```
Par contre ceci n'arrive pas avec la version monomorphe:Kim NguyễnKim Nguyễnhttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/19repeated definitions bring bugs in the toplevel2021-05-02T15:37:53+02:00Giuseppe Castagnarepeated definitions bring bugs in the toplevelDefine the following flatten function in the toplevel:
````
type Tree('a) = ('a\[Any*]) | [ (Tree('a))* ]
let flatten ( (Tree('a)) -> ['a*])
| [] -> []
| [h ;t] -> (flatten h)@(flatten t)
| x -> [x];;
# flatten [ 3 'r' [ 4 [ `true 5 ]] [ "quo" [[ `false ] "stop" ] ] ];;
- : [ (Bool | 3--5 | 'o'--'u')* ] = [ 3 'r' 4 true 5 'quo' false 'stop' ]
````
now define it a second time in the toplevel
````
let flatten ( (Tree('a)) -> ['a*])
| [] -> []
| [h ;t] -> (flatten h)@(flatten t)
| x -> [x];;
# flatten [ 3 'r' [ 4 [ `true 5 ]] [ "quo" [[ `false ] "stop" ] ] ];;
- : [ (Bool | 3--5 | 'o'--'u')* ] = [ [ 3
'r'
[ 4 [ true 5 ] ]
[ "quo" [ [ false ] "stop" ] ]
]
]
````
duh? It has become the identity function and with the wrong type.Define the following flatten function in the toplevel:
````
type Tree('a) = ('a\[Any*]) | [ (Tree('a))* ]
let flatten ( (Tree('a)) -> ['a*])
| [] -> []
| [h ;t] -> (flatten h)@(flatten t)
| x -> [x];;
# flatten [ 3 'r' [ 4 [ `true 5 ]] [ "quo" [[ `false ] "stop" ] ] ];;
- : [ (Bool | 3--5 | 'o'--'u')* ] = [ 3 'r' 4 true 5 'quo' false 'stop' ]
````
now define it a second time in the toplevel
````
let flatten ( (Tree('a)) -> ['a*])
| [] -> []
| [h ;t] -> (flatten h)@(flatten t)
| x -> [x];;
# flatten [ 3 'r' [ 4 [ `true 5 ]] [ "quo" [[ `false ] "stop" ] ] ];;
- : [ (Bool | 3--5 | 'o'--'u')* ] = [ [ 3
'r'
[ 4 [ true 5 ] ]
[ "quo" [ [ false ] "stop" ] ]
]
]
````
duh? It has become the identity function and with the wrong type.https://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 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).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/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, 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
```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 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 doneThe 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 -> Bool & Int -> Int;;
Bool -> Arrow
```
here we cannot paste the output of the toplevel.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ễnhttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/1Try to improve the parsing of ; in record expressions.2021-05-02T14:45:46+02:00Kim NguyễnTry to improve the parsing of ; in record expressions.Some expressions are more binding than ; and therefore make its use clumsy in record expressions :
```
# let x = { a = ref Int 2 ; b = 42 } ;;
Characters 29-30:
Unbound identifier 'b'
# let x = { b = 42 ; a = ref Int 2 } ;;
val x : { a={ get=[ ] -> Int set=Int -> [ ] } b=42 } = {
a={ get=<fun>
set=<fun> }
b=42 }
# let x = { a = (ref Int 2) ; b = 42 } ;;
val x : { a={ get=[ ] -> Int set=Int -> [ ] } b=42 } = {
a={ get=<fun>
set=<fun> }
b=42 }
```Some expressions are more binding than ; and therefore make its use clumsy in record expressions :
```
# let x = { a = ref Int 2 ; b = 42 } ;;
Characters 29-30:
Unbound identifier 'b'
# let x = { b = 42 ; a = ref Int 2 } ;;
val x : { a={ get=[ ] -> Int set=Int -> [ ] } b=42 } = {
a={ get=<fun>
set=<fun> }
b=42 }
# let x = { a = (ref Int 2) ; b = 42 } ;;
val x : { a={ get=[ ] -> Int set=Int -> [ ] } b=42 } = {
a={ get=<fun>
set=<fun> }
b=42 }
```Kim NguyễnKim Nguyễnhttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/5Opposite operator on variables2021-05-02T14:39:48+02:00Kim NguyễnOpposite operator on variablesWhile you can write in CDuce ``-42`` the following is not allowed :
```
# let x = 3 in - x;;
Characters 10-12:
Parsing error: [expression level top] expected after "in" (in [phrase])
```While you can write in CDuce ``-42`` the following is not allowed :
```
# let x = 3 in - x;;
Characters 10-12:
Parsing error: [expression level top] expected after "in" (in [phrase])
```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 : '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>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/11"ref", several errors in parsing and typing2021-05-02T14:31:30+02:00Kim Nguyễn"ref", several errors in parsing and typingHere you are some bugs with refs:
<pre>
# type X ('a) = ref 'a;;
Characters 14-17:
Parsing error: [phrase] or ";;" expected (in [toplevel phrases])
# type X ('a) = ref ('a) ;;
Characters 14-22:
Unknown parametric type ref
# type X ('a) = ref Int ;;
Characters 5-6:
Capture variable not allowed: ref
# type X = ref Int ;;
Characters 5-6:
Capture variable not allowed: ref
# type X = (ref Int) ;;
Characters 11-14:
Capture variable not allowed: ref
</pre>
and a typo
<pre>
let x = ref ('a -> 'a) (fun (x:'b):'b = x);;
Characters 9-44:
Type ref 'a -> 'a constains polymorphic variables
^^^^
</pre>Here you are some bugs with refs:
<pre>
# type X ('a) = ref 'a;;
Characters 14-17:
Parsing error: [phrase] or ";;" expected (in [toplevel phrases])
# type X ('a) = ref ('a) ;;
Characters 14-22:
Unknown parametric type ref
# type X ('a) = ref Int ;;
Characters 5-6:
Capture variable not allowed: ref
# type X = ref Int ;;
Characters 5-6:
Capture variable not allowed: ref
# type X = (ref Int) ;;
Characters 11-14:
Capture variable not allowed: ref
</pre>
and a typo
<pre>
let x = ref ('a -> 'a) (fun (x:'b):'b = x);;
Characters 9-44:
Type ref 'a -> 'a constains polymorphic variables
^^^^
</pre>Kim NguyễnKim Nguyễnhttps://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/15Tallying error with recursive types2021-05-02T10:37:10+02:00Tommaso PetruccianiTallying error with recursive typesIn the presence of recursive types and using a non-empty `delta`, we get wrong solutions for tallying. For
~~~
# debug tallying ['a] [ [] -> [] , [(Int 'a)*] -> [] ];;
~~~
we get the empty solution.
As a result, in CDuce, we have
~~~
# let f (x: []): [] = x;;
val f : [ ] -> [ ] = <fun>
# let g (l: [(Int 'a)*]): [] = f l;;
val g : [ (Int 'a)* ] -> [ ] = <fun>
# g [1 2];;
- : [ ] = [ 1 2 ]
~~~
where a non-empty list is given type `[ ]`.
(Kim, I'm not sure if it's the same problem you mentioned yesterday of the incorrect use of memoization.)In the presence of recursive types and using a non-empty `delta`, we get wrong solutions for tallying. For
~~~
# debug tallying ['a] [ [] -> [] , [(Int 'a)*] -> [] ];;
~~~
we get the empty solution.
As a result, in CDuce, we have
~~~
# let f (x: []): [] = x;;
val f : [ ] -> [ ] = <fun>
# let g (l: [(Int 'a)*]): [] = f l;;
val g : [ (Int 'a)* ] -> [ ] = <fun>
# g [1 2];;
- : [ ] = [ 1 2 ]
~~~
where a non-empty list is given type `[ ]`.
(Kim, I'm not sure if it's the same problem you mentioned yesterday of the incorrect use of memoization.)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 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.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/14Tallying: monomorphic variables are not handled correctly2021-05-02T10:19:11+02:00Tommaso PetruccianiTallying: monomorphic variables are not handled correctlyWhen we perform tallying with a non-empty delta and types contain
top-level variables that are in delta, we do not handle them correctly.
See
~~~
debug tallying ['b] [ ('a, Int) , 'b ];;
~~~
(no solution found, while `'a<-Empty` works) and
~~~
debug tallying ['b] [ ('a, Int) , 'b | 'c ];;
~~~
(no solution found, while it works if we use `['c]` as delta instead).
The problem is in Type_tallying.toplevel (line 245).
We can probably fix it as follows. Currently, we always pick the first variable (positive or negative) that we find (we give priority to polymorphic ones only in one branch of matching). Instead, as long as there is at least one polymorphic variable, we should prefer it to monomorphic ones.
If all variables are monomorphic, we should basically test for emptiness of the type without these monomorphic variables. Say the smallest variable is `'a` and is positive; thus we have `t & 'a`. For emptiness we need `t <: not('a)`. However, this should be possible only if `t` contains `not('a)` (which maybe never happens because we would have simplified the type?) or if it is empty (which we surely need to check).When we perform tallying with a non-empty delta and types contain
top-level variables that are in delta, we do not handle them correctly.
See
~~~
debug tallying ['b] [ ('a, Int) , 'b ];;
~~~
(no solution found, while `'a<-Empty` works) and
~~~
debug tallying ['b] [ ('a, Int) , 'b | 'c ];;
~~~
(no solution found, while it works if we use `['c]` as delta instead).
The problem is in Type_tallying.toplevel (line 245).
We can probably fix it as follows. Currently, we always pick the first variable (positive or negative) that we find (we give priority to polymorphic ones only in one branch of matching). Instead, as long as there is at least one polymorphic variable, we should prefer it to monomorphic ones.
If all variables are monomorphic, we should basically test for emptiness of the type without these monomorphic variables. Say the smallest variable is `'a` and is positive; thus we have `t & 'a`. For emptiness we need `t <: not('a)`. However, this should be possible only if `t` contains `not('a)` (which maybe never happens because we would have simplified the type?) or if it is empty (which we surely need to check).Kim NguyễnKim Nguyễn