cduce issues https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues 2021-05-02T10:41:43+02:00 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 https://gitlab.math.univ-paris-diderot.fr/cduce/cduce/-/issues/9 Polymorphic typing of record operations 2017-10-16T08:48:07+02:00 Kim Nguyễn Polymorphic typing of record operations How to type the operations on records, concatenation e1 + e2 and field suppression e\ l in the presence of polymorphic variables. For the time being we do a safe but gross approximation. For instance ``` &#39;a &amp; r \ l = r \ l ``` Can ... How to type the operations on records, concatenation e1 + e2 and field suppression e\ l in the presence of polymorphic variables. For the time being we do a safe but gross approximation. For instance ``` 'a & r \ l = r \ l ``` Can we do better?