Kakadu
March 31, 2021, 6:44pm
62
lpw25:
This requires us to answer questions like: “Is there any module X such that the result of Print_list(X) would be of the required module type?”. Which is actually just= Print_list(?X) with sig type t = int list val print : ... , where ?X is a unification variable and = ... is a singleton type/module alias.
So implementing modular implicits requires us to implement a unification algorithm at the module level. Now the prototype uses a very naive algorithm which is very weak and quite unpredictable. My more ambitious plan is to implement a higher-order pattern unification, of the sort found in languages like Agda, and to do so for the full module language. My plan also includes strengthening the module language with additional equalities – in particular module aliases on functor applications and eta-equality on structures – in order for unification to have some more desirable properties.
I can’t figure out an example where high-order unification is important and naive unification is not enough. Can you point on the one so I could study it?
P.S. Sorry for necroposting
2 Likes
