How would I phrase this flatten func in MLStruct?

[metaleap]

Having not (yet) laboured through your 2024 MLStruct Type Inference 181-pager, I still wanted to see in your web playground how the below function will be type-inferenced in MLStruct, ML-ish pseudocode taken from Castagna et al 2024: Polymorphic Type Inference for Dynamic Languages where I just found that very interesting case of a polymorphic function that's technically "just" Any -> [Any] but invites more specific typing in a intersection/union/negation-supported type-inferencing setup:

let rec flatten x = match x with
| [] -> []
| h :: t -> concat ( flatten h ) ( flatten t )
| _ -> [x]

Would you mind a quick transcription to MLStruct here I can paste into https://hkust-taco.github.io/mlstruct/ editor, so I can try it out? Many thanks in advance!

[LPTK]

Hi @metaleap. Thanks for your interest in this project!

Here's how you implement your function in MLstruct:

class Nil
class Cons[A]: { h: A; t: List[A] }
type List[A] = Cons[A] | Nil

def concat: List['a] -> List['a] -> List['a]
rec def concat x y = case x of
  Nil -> y,
  Cons -> Cons { h = x.h; t = concat x.t y }

rec def flatten x = case x of
  Nil -> Nil{},
  Cons -> concat (flatten x.h) (flatten x.t),
  _ -> Cons { h = x; t = Nil{} }

You can try it in the web demo or in the project's diff-tests, which yield the following output:

class Nil
class Cons[A]: { h: A; t: List[A] }
type List[A] = Cons[A] | Nil
//│ Defined class Nil
//│ Defined class Cons[+A]
//│ Defined type alias List[+A]

def concat: List['a] -> List['a] -> List['a]
rec def concat x y = case x of
  Nil -> y,
  Cons -> Cons { h = x.h; t = concat x.t y }
//│ concat: List['a] -> List['a] -> List['a]
//│       = <missing implementation>
//│ 'a -> 't -> 't
//│   where
//│     't :> Cons['A] & {h: 'h, t: 't}
//│        <: List['A]
//│     'a <: #Cons & {h: 'h & 'A, t: 'a} | Nil
//│   <:  concat:
//│ List['a] -> List['a] -> List['a]
//│       = [Function: concat1]

rec def flatten x = case x of
  Nil -> Nil{},
  Cons -> concat (flatten x.h) (flatten x.t),
  _ -> Cons { h = x; t = Nil{} }
//│ flatten: 'a -> (Cons['h] & {t: Nil} | Nil | List['h])
//│   where
//│     'a <: #Cons & {h: 'a, t: 'a} | Nil | 'h & ~#Cons & ~#Nil
//│        = [Function: flatten]

c1 = Cons { h = 123; t = Nil{} }
//│ c1: Cons[123] & {t: Nil}
//│   = Cons { h: 123, t: Nil {} }

flatten c1
//│ res: Cons[123] & {t: Nil} | Nil | List[123]
//│    = Cons { h: 123, t: Nil {} }

c2 = Cons { h = c1; t = c1 }
//│ c2: Cons[123 | Cons[123] & {t: Nil}] & {h: Cons[123] & {t: Nil}, t: Cons[123] & {t: Nil}}
//│   = Cons { h: Cons { h: 123, t: Nil {} }, t: Cons { h: 123, t: Nil {} } }

flatten c2
//│ res: Cons[123] & {t: Nil} | Nil | List[123]
//│    = Cons { h: 123, t: Cons { h: 123, t: Nil {} } }

The main differences with Castagna's work is that:

• MLstruct doesn't intend to support intersection-based overloading.
• This notably allows MLstruct to avoid all backtracking in the type inference algorithm, making it efficient and scalable.
• MLstruct infers principal types, meaning that all terms have a most general type that is inferred by the algorithm. By contrast, in the paper you linked, type annotations are sometimes necessary.