Implement lazy generalization

[azdavis]

Environment

• Millet version: v0.8.5

Steps to reproduce

https://github.com/MLton/mltonlib/blob/04477d37e709c3bcff9c26a9b00494ee85469f34/com/ssh/generic/unstable/detail/value/pretty.sml#L55-L67

Expected behavior

millet does not hang

Actual behavior

millet hangs

[azdavis]

smaller reproducer follows. the problem is not with the & but rather with type-checking the commented out line marked BAD.

structure Product = struct
  datatype ('a, 'b) product = & of 'a * 'b

  type ('a, 'b) t = ('a, 'b) product
end

structure UnOp = struct
  type 'a t = 'a -> 'a
end

structure Iso = struct
  type ('a, 'b) t = ('a -> 'b) * ('b -> 'a)
end

structure CPS = struct
  type ('a, 'b) t = ('a -> 'b) -> 'b
end

signature STATIC_SUM = sig
  type ('dL, 'cL, 'dR, 'cR, 'c) dom
  type ('dL, 'cL, 'dR, 'cR, 'c) cod
  type ('dL, 'cL, 'dR, 'cR, 'c) t = ('dL, 'cL, 'dR, 'cR, 'c) dom -> ('dL, 'cL, 'dR, 'cR, 'c) cod
end

signature FOLD = sig
  type ('a, 'b, 'c) t
  type ('s1, 's2, 'r) s = 's1 -> ('s2, 'r) CPS.t
  type ('a, 's1, 's2, 'r) s1 = 's1 -> 'a -> ('s2, 'r) CPS.t
  val $ : ('a, 'a, 'b) t -> 'b
end

signature FRU = sig
  structure Fold : FOLD
  structure StaticSum : STATIC_SUM
  type ('rec, 'upds) t'
  type ('rec, 'upds, 'data) t = (('rec, 'upds) t', ('rec, 'upds) t', 'data UnOp.t) Fold.t
  val fru : (((('a -> unit) * 'b UnOp.t, 'c, 'd, 'e, 'c) StaticSum.t, ('f, 'f, 'g, 'g, (('h -> 'rec UnOp.t) -> 'prod_upds) * ('h -> 'prod UnOp.t)) StaticSum.t, ('rec, 'prod) Iso.t -> ('upds, 'prod_upds) Iso.t -> (('rec, 'upds, 'rec) t, 's) CPS.t) Fold.t, 't) CPS.t
  val A : ((('a * 'b, 'c UnOp.t * ('d -> 'e -> 'd), (('f -> 'g) -> 'h) * ('i -> 'j -> 'k), ((('f, 'l, 'm, 'l, 'l) StaticSum.t -> 'g) -> ('h, 'm -> 'g) Product.t) * (('i, ('j, 'n) Product.t -> ('k, 'n) Product.t, 'o, ('p, 'q) Product.t -> ('p, 'o) Product.t, 'r) StaticSum.t -> 'r), 's) StaticSum.t, 't, 'u) Fold.t, (('v, 'w, 's, 'x, 'x) StaticSum.t, 't, 'u) Fold.t, 'y) Fold.s
  val U : ('upds -> 'val -> 'rec UnOp.t) -> 'val -> ((('rec, 'upds) t', ('rec, 'upds) t', 'result) Fold.t, (('rec, 'upds) t', ('rec, 'upds) t', 'result) Fold.t, 'k) Fold.s
end

functor F (FRU : FRU) = struct
  open FRU Product

  infix &

  fun f1 {a = a, b = b, c = c, d = d, e = e, f = f, g = g, h = h, i = i} = a & b & c & d & e & f & g & h & i

  fun f2 (a & b & c & d & e & f & g & h & i) = {a = a, b = b, c = c, d = d, e = e, f = f, g = g, h = h, i = i}

  val ~ = (f1, f2)

  (* BAD *)
  (* fun u f v = fru A A A A A A A A A Fold.$ ~ ~ (U f v) Fold.$ *)
end

[azdavis]

the culprit appears to be the usage of 'fru' aka functional record update.

according to the fru sig, we should check http://mlton.org/FunctionalRecordUpdate for more info. this page give a different implementation of fru than the one currently checked in to mlton lib. it also says at the bottom of the page:

Efficiency

Before Sep 14, 2009, this page advocated an alternative implementation of FunctionalRecordUpdate. However, the old structure caused exponentially increasing compile times. We advise you to switch to the newer version.

looking at the current impl of fru in mlton lib, given that the last updated timestamp is Jan 8, 2009, i suspect that this is indeed the 'older version' alluded to with exponentially increasing compile times.

i thus lean towards closing this as wontfix since this is a pathological case. i'm reluctant to invest significant time into optimizing the millet typechecker for cases like this.

[azdavis]

possible optimization opportunities:

• structural type sharing to reduce allocations
• https://okmij.org/ftp/ML/generalization.html

[azdavis]

did the first one (structural sharing) but it's still slow

[azdavis]

changing this to be an enhancement request to implement https://okmij.org/ftp/ML/generalization.html, which should make millet as a whole generally faster