F* Code Generation

paradox generate --fstar [--path PATH]

Product Types

Input:

type Person
  name: Text
  age: Integer
  admin: Boolean

Output:

type person =
{ name : string
; age : int
; admin : bool
}

Type names are snake_cased per F* convention.

Union Types

Unions become F* inductive types with GADT-style constructors:

type role =
| Admin : role
| Editor : string -> role
| Viewer : role

Wrap Types

Wraps generate type abbreviations with wrap/unwrap helpers:

type email = string

let wrap_email (v : string) : email = v

let unwrap_email (v : email) : string = v

Validators

Validation generates either string t result functions, ready for refinement type lifting:

let valid_email (value : string) : either string email =
  if not (value <> "") then Inl "Validation failed: unwrap != \"\""
  else Inr (wrap_email value)

let is_valid_email (value : string) : bool =
  match valid_email value with Inr _ -> true | Inl _ -> false

The is_valid_ predicates can be used directly as F* refinement predicates:

type checked_email = x:string{is_valid_email x == true}

Notes

  • No JSON serialization is generated (F* has no standard JSON library)

  • Sets are represented as sorted lists

  • Maps are represented as association lists of tuples

See Also