Unifying ADTs in ADTs fails in top-level binding

[j14159]

Excerpt from an Alpaca-native AST that demonstrates the unification failure:

module example_ast

export float, line

type symbol = Symbol {line: int, name: string, original: string}

type int_exp = Int {line: int, i: int}
type float_exp = Float {line: int, f: float}
type string_exp = String {line: int, value: string}

{- Expressions are only permitted inside of top-level bindings.
 -}
type expr = int_exp
          | float_exp
          | string_exp
          | symbol

let line Float {line=l} = l
let line Int {line=l} = l
let line Symbol {line=l} = l
let line String {line=l} = l

let  float l f = Float {line=l, f=f}

This will fail, reporting that the typer cannot unify int_exp and float_exp. I'm reasonably certain that this is happening because alpaca_typer:unify_adt/6 sees two different ADTs, the only thing it tries to do is see if one fits inside of the other. In principle this shouldn't be too hard to fix but there might be performance considerations.

Things I don't know yet:

• does the above example work in something like OCaml/Elm?
• should the above example work in Alpaca? This might get nastier in the typer if we want to add a switch to force decidability, e.g. something that rejects type t = int | float as checking unions/sums like the above example could get expensive.

[lepoetemaudit]

You cannot do this in Elm or OCaml because all unions must be explicitly qualified, e.g.

type expr = int_exp | float_exp | string_exp | symbol

Is invalid - you'd have to write something like:

type expr = IntExpr of int_expr | FloatExpr of float_expr (* etc *)

If the line was outside the symbol, say as part of a tuple, you could have a generic function that takes a two-tuple, something of type:

fn (symbol, int) -> int

As far as I'm aware none of the MLs with ADTs support this sort of construct. Perhaps it could be achieved with typeclasses but you'd still need to extract the data for each union first in a pattern match or some such.

[j14159]

Makes sense to me, thanks. Maybe leaving the type error in place is better than trying to satisfy that union.