cduce issues https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues 2022-02-01T17:00:39+01:00 https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/26 Weak polymorphism is not unified nor propagated when used in a function 2022-02-01T17:00:39+01:00 Mattias Weak polymorphism is not unified nor propagated when used in a function Some examples here: ```ocaml # let r = ref ([ &#39;a* ]) [];; val r : { get=[ ] -&gt; [ &#39;_weak0* ] set=[ &#39;_weak0* ] -&gt; [ ] } = { get=&lt;fun&gt; # let f (x : Int) : Int = r := [ x ]; x + 1;; val f : Int -&gt; Int = &lt;fun&gt; # r;; - : { get=[ ] -&gt; [ &#39;_... 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ễn Kim Nguyễn https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/25 Issue in apply that makes it not monotone 2022-01-30T14:35:33+01:00 Mickael Laurent Issue in apply that makes it not monotone 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 ... 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ễn Kim Nguyễn https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/17 Unsoundness with record typing 2021-05-02T10:41:43+02:00 Tommaso Petrucciani Unsoundness with record typing Functions on records can be given unsound types as in the following: # let f = fun ({..} -&gt; &#39;a) x -&gt; x;; val f : Record -&gt; &#39;a = &lt;fun&gt; # f {};; - : &#39;a = { } It seems that this `&#39;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 failed Kim Nguyễn Kim Nguyễn https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/12 Solving type equation with recursive types for a variable &#39;a does not work wh... 2017-10-16T08:48:07+02:00 Kim Nguyễn Solving type equation with recursive types for a variable 'a does not work when 'a occurs below a union/intersection/negation 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: ``` ... 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ễn Kim Nguyễn