Polymorphic Recursion

[EthanOlpin]

I wasn't able to find other discussions around this topic, very sorry if this has been discussed already.

The following code fails to build because Gleam is unable to infer that the type parameter changes in the recursive call.

type Nested(a) {
  Cons(a, Nested(List(a)))
  Epsilon
}

fn length(nested: Nested(a)) -> Int {
  case nested {
    Cons(_, n) -> 1 + length(n)
    Epsilon -> 0
  }
}

  │
8 │     Cons(_, n) -> 1 + length(n)
  │                               ^

Expected type:

    Nested(a)

Found type:

    Nested(List(a))

It seems like this might indicate that Gleam lacks support for polymorphic recursion. Creating a const alias for the function seems to be a workaround for this scenario:

type Nested(a) {
  Cons(a, Nested(List(a)))
  Epsilon
}

fn length(nested: Nested(a)) -> Int {
  case nested {
    Cons(_, n) -> 1 + length_rec(n)
    Epsilon -> 0
  }
}

const length_rec = length

However I wasn't able to isolate why the workaround fails in this more complex (and more contrived) example:

pub type Node(a) {
  One(a)
  Two(a, a)
}

pub type Pairings(a) {
  Empty
  Deep(Node(a), Pairings(Node(a)))
}

pub fn push(a, pairings: Pairings(a)) -> Pairings(a) {
  case pairings {
    Empty -> Deep(One(a), Empty)
    Deep(One(b), m) -> Deep(Two(a, b), m)
    Deep(Two(b, c), m) -> Deep(One(a), push_rec(Two(b, c), m))
  }
}

const push_rec = push

Which fails with:

   │
15 │     Deep(Two(b, c), m) -> Deep(One(a), push_rec(Two(b, c), m))
   │                                                 ^^^^^^^^^

Expected type:

    a

Found type:

    Node(a)

I just had a couple questions:

1. Is polymorphic recursion something that Gleam could feasibly support in the future and does it warrant further discussion? (Is "polymorphic recursion" even the correct name for the thing I'm asking about here?)
2. What workarounds exist for the second scenario / is there a more general solution for both issues?

[EthanOlpin]

I see now that adding a type annotation to the const alias allows the second case to build. i.e. the compiler is happy with this:

pub type Node(a) {
  One(a)
  Two(a, a)
}

pub type Pairings(a) {
  Empty
  Deep(Node(a), Pairings(Node(a)))
}

pub fn push(v: a, pairings: Pairings(a)) -> Pairings(a) {
  case pairings {
    Empty -> Deep(One(a), Empty)
    Deep(One(b), m) -> Deep(Two(a, b), m)
    Deep(Two(b, c), m) -> Deep(One(a), push_rec(Two(b, c), m))
  }
}

const push_rec: fn(a, Pairings(a)) -> Pairings(a) = push

I feel that the language tour could be a bit more clear on this point. Unless I'm mistaken this seems like a case where the type annotation helped the compiler, but the following statement left me with the impression that you could remove annotations from a compiling program and expect it to still compile.

Type annotations may be useful for documentation purposes, but they do not change how Gleam type checks the code beyond ensuring that the annotation is correct.

Could that part of the tour be made more clear? Or is there actually a bug here that makes the annotation necessary?

[lpil]

@hayleigh-dot-dev can you see any reason why we wouldn't support this without the indirection?

[hayleigh-dot-dev]

Yeah, type inference for polymorphic recursion is undecidable, actually! The ocaml docs have an ok description of the general problem here and their solution requires universal quantification. Haskell has a similar problem and solution.

Gleam couldn't be changed to support no indirection without also adding universal quantification, which I think we wouldn't want.

[lpil]

Wow! Thank you for all the detail, very helpful