Problem

Vera has no way to convert any value to a String. This affects every type in the language: primitives (Int, Nat, Float64, Bool), compound types (Array<T>, tuples), ADTs (List<T>, Option<T>, user-defined types), and refinement types. Without this:

• IO.print can only output string literals, not computed values
• Entry-point functions that compute results cannot display them via main (which requires @Unit -> @Unit with IO effects per spec section 5.11)
• There is no way to inspect or debug values at runtime
• Examples must use test_* functions returning typed values and rely on vera run --fn to print the WASM result, rather than having self-contained main functions

Proposed design

A general-purpose stringification mechanism that works for any type, not just a handful of builtins. Possible approaches:

Option A: Built-in show function (compiler-derived)

The compiler automatically generates string representations for all types:

-- Works for any type, compiler synthesises the implementation
show(@Int -> @String)
show(@Array<Int> -> @String)
show(@List<Option<Int>> -> @String)

Option B: Typeclass / trait (user-extensible)

A Show or Display trait that the compiler derives for built-in types and users implement for custom types:

-- Compiler-derived for primitives and ADTs
-- User can override for custom formatting

Option C: Minimal builtins + string interpolation

Provide primitive converters and let string interpolation handle composition:

int_to_string(@Int -> @String)
float_to_string(@Float64 -> @String)
bool_to_string(@Bool -> @String)
-- Plus string interpolation or concatenation for compound types

Scope

At minimum this needs to cover:

• Primitives: Int, Nat, Float64, Bool
• Strings: identity (already a string)
• Arrays: Array<T> where T is showable
• ADTs: List<T>, Option<T>, Either<L, R>, and any user-defined data type
• Refinement types: delegates to the underlying type
• Tuples / multi-field constructors: e.g. Cons(1, Cons(2, Nil)) -> "Cons(1, Cons(2, Nil))"

Implementation notes

• Primitive conversions likely need to be compiler builtins or WASM imports since string allocation requires runtime support
• Recursive/compound type stringification needs the compiler to walk the type structure
• This ties into the broader stdlib/runtime story (see runtime/ directory)
• May also interact with future string interpolation features

Context

Discovered while making examples runnable (#107): we wanted public fn main(@Unit -> @Unit) effects(<IO>) entry points that print computed results, but there is no mechanism to convert any non-string value to String for IO.print.