How to type polymorphic variants with open generic functions?

I'd like to implement a language with polymorphic variants, but instead of using pattern matching, I'd like to use Common Lisp-like generic functions that are defined with define-generic, and to which cases can be added with define-method.

Where in pseudo-ML I'd say

let length list =
  case list of 
    `Nil -> 0
  | `Cons _ cdr -> 1 + length cdr

in my language I'd say

(define-generic length)
(define-method (length `Nil) 0) 
(define-method (length (`Cons _ cdr)) (+ 1 (length cdr))) 

I'd like to able to add methods in different compilation units, and only type-check generic functions at the end of compile-time, once all methods are known. Another possibility might be to defer type checking of generic functions to link time.

Any ideas or pointers to things I should check out? I'm currently reading Simple Type Inference for Structural Polymorphism, and TAPL is lying on the coffee table.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

compile time, link time -- the distinction is fuzzy.

By the fact that you refer to a "link time" I infer that you intend to have a build model with separate compilation. That's fine; there's no good reason to put off type checking.

Have a look at the Allegro CL source. It uses a two-target compilation model where each source unit compiled creates an "interface" with type info, and also a linkable with the executable code. The key point here is that the "interface" is only updated if it changes, which for most small adjustments it doesn't. That means that other units which don't need recompiling unless the interface changes don't have to get recompiled. Type errors in method calls, like type errors in any function call, get detected at compile time, and linking proceeds normally.

Bear

It's probably good to

It's probably good to revisit that paper, of course, but I cannot help but notice a recurring theme in the authorship of the LtU nodes... :)

Didn't notice that Manuel

Didn't notice that Manuel had posted that link. Still, sometimes applicability isn't always obvious. Take normal algebraic type declarations, have each case introduce its own subtype to the algebraic type, then apply the linked paper for overload resolution.

Also relevant and keeping more with ML semantics: Extensible Programming with First-Class Cases. I know for certain Manuel didn't post that article. :-)

Maybe reframe the question

How do we type modules that expose open functions and data?

I wonder if mixins or traits models would be appropriate? The module is exposing various provisions and requirements. If left implicit, many of the challenges that "traits" solve relative to mixins (regarding commutative composition) will still be part of your language.

To take module systems seriously is to reify them.