Search code examples
webassembly

How to understand the recursive types in Wasm?


How to understand the difference between the two snippets of code? The spec says that a rec definition defines a group of mutually recursive types that can refer to each other. But for the first snippet which isn't surrounded by a rec block, it could pass the compilation of Binaryen which seems to be fine to me.

Spec: https://github.com/WebAssembly/gc/blob/main/proposals/gc/MVP.md#type-definitions

(module
  (type $f1 (func)) 
  (type (struct (field (ref $f1))))
)
(module
  (rec
    (type $f1 (func)) 
    (type (struct (field (ref $f1))))
  )
)

But if I pull the code from the first snippet into the below snippet, there would be an error occurred "[wasm-validator error in module] global init must have correct type"

(module
  (type $f1 (func)) 
  (type (struct (field (ref $f1))))
  (rec (type $f2 (func)) (type (struct (field (ref $f2)))))
  (func $f (type $f2))
  (global (ref $f1) (ref.func $f))
)

Solution

  • Your first module is in fact interpreted as a short-hand for:

    (module
      (rec
        (type $f1 (func)) 
      )
      (rec
        (type (struct (field (ref $f1))))
      )
    )
    

    That is, it defines two separate groups of recursive types (even though neither is actually recursive). The factoring of types into recursion groups matters for type equivalence: two types are only deemed equivalent when they are defined at the same position in equivalently structured recursion groups.

    The reasons for this seemingly restrictive semantics are rather technical, but boil down to having a linear algorithm for deciding type equivalence and performing type canonicalisation, which is important to keep validation in engines tractable.

    Edit: Technically, these are called iso-recursive types, as opposed to the more liberal equi-recursive types, where every type is implicitly equivalent to its unrolling. See Wikipedia for a super-brief explanation.