Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
54 changes: 54 additions & 0 deletions design/WhitePaper.md
Original file line number Diff line number Diff line change
Expand Up @@ -159,6 +159,60 @@ Finally, it would sometimes be desirable to have extended syntax for multi-line
The Motoko type system has a number of known gaps that stand in the way of certain forms of abstraction and composition.


#### Newtypes

Motoko supports `newtype` declarations that introduce a nominal wrapper around an existing type.
Unlike `type` aliases (which are structurally transparent), a `newtype` is fully opaque: no implicit conversion exists between the newtype and its underlying representation.

```
newtype Time = Int;
let t : Time = Time(123); // explicit wrapping via constructor
let n : Int = t.unwrap; // explicit unwrapping via .unwrap
```

The declaration introduces both a type `Time` and a value `Time` — the constructor function of type `Int -> Time`.

Newtypes can have type parameters.
Variance of each type parameter is computed from its usage in the right-hand side, consistent with how `type` aliases work:

```
newtype Map<K, V> = MapInternals<K, V>;
let m : Map<Text, Nat> = Map<Text, Nat>(internal);
let i = m.unwrap; // : MapInternals<Text, Nat>
```

##### Semantics

- **Opacity.** A newtype `T` and its underlying type `U` are distinct for subtyping and equality. `T </: U` and `U </: T`. Values must be explicitly wrapped/unwrapped.
- **Zero-cost.** At runtime, newtype values have the same representation as the underlying type. The constructor and `.unwrap` are identity operations.
- **Nominal.** Two newtypes with the same underlying type are distinct: `newtype A = Int` and `newtype B = Int` produce incompatible types.
- **Constructor.** The newtype name is bound as both a type and a value (the constructor function). For `newtype T<A> = U<A>`, the constructor has type `<A>(U<A>) -> T<A>`.
- **Unwrap.** Values of newtype are given a virtual `.unwrap` field (analogous to how arrays have `.size`). For a value `v : T<A>`, `v.unwrap : U<A>`.

##### Candid Serialization

Newtypes are a Motoko-only concept. When serializing to Candid, newtypes are transparent: `Time` serializes as `Int`, `Map<K, V>` serializes as its underlying record type.

##### Stable Storage and Migrations

For `.most` files (stable type signatures), newtypes are treated like type aliases. This allows users to freely add, rename, or remove newtypes across upgrades without breaking migration compatibility.

Newtypes are preserved in error messages (e.g., `Time` rather than `Int`) for better diagnostics.

##### Implementation

The `newtype` declaration introduces a new type constructor kind `Newtype(binds, body)` alongside the existing `Def` (transparent alias) and `Abs` (abstract/parameter). Key design choices:

- **`normalize`** does *not* expand `Newtype`, preserving opacity during type checking. This is the fundamental difference from `Def`.
- **`promote`** does *not* expand `Newtype`, preventing implicit promotion in subtyping contexts.
- **Lowering.** During desugaring, `Newtype` kinds are mutated to `Def`, making them transparent for downstream IR passes and codegen. The constructor is emitted as an identity function binding.

##### Future Work

- Pattern matching on newtypes.
- Methods on newtypes.


#### Type Fields ([#760](https://github.com/dfinity/motoko/issues/760))

Motoko allows type members in objects and modules:
Expand Down
1 change: 1 addition & 0 deletions doc/md/examples/grammar.txt
Original file line number Diff line number Diff line change
Expand Up @@ -335,6 +335,7 @@
<dec_nonvar> ::=
'let' <pat> '=' <exp>
'type' <id> ('<' <list(<typ_bind>, ',')> '>')? '=' <typ>
'newtype' <id> ('<' <list(<typ_bind>, ',')> '>')? '=' <typ>
<shared_pat_opt> 'func' <func_pat> (':' <typ>)? <func_body>
<parenthetical>? <obj_or_class_dec>
'mixin' <pat_plain> <obj_body>
Expand Down
2 changes: 1 addition & 1 deletion src/docs/extract.ml
Original file line number Diff line number Diff line change
Expand Up @@ -224,7 +224,7 @@ struct
} )
| _ -> Some (mk_xref (Xref.XValue name), extract_value_doc Var rhs name)
)
| Source.{ it = Syntax.TypD (name, ty_args, typ); _ } ->
| Source.{ it = Syntax.TypD (name, ty_args, typ) | Syntax.NewtypeD (name, ty_args, typ); _ } ->
let doc_typ =
match typ.it with
| Syntax.ObjT (_, fields) ->
Expand Down
3 changes: 2 additions & 1 deletion src/docs/namespace.ml
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,8 @@ let from_module =
(StringMap.of_seq (List.to_seq bound_names))
acc.values;
}
| Syntax.TypD (id, _, _) ->
| Syntax.TypD (id, _, _)
| Syntax.NewtypeD (id, _, _) ->
{
acc with
types = StringMap.add id.it (mk_xref (Xref.XType id.it)) acc.types;
Expand Down
1 change: 1 addition & 0 deletions src/gen-grammar/grammar.sed
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,7 @@ s/VAR/\'var\'/g
s/SHROP/\' >>\'/g
s/SHRASSIGN/\'>>=\'/g
s/UNDERSCORE/\'_\'/g
s/NEWTYPE/\'newtype\'/g
s/TYPE/\'type\'/g
s/TRANSIENT/\'transient\'/g
s/TRY/\'try\'/g
Expand Down
5 changes: 3 additions & 2 deletions src/ir_def/check_ir.ml
Original file line number Diff line number Diff line change
Expand Up @@ -197,7 +197,8 @@ let rec check_typ env typ : unit =
List.iter (check_typ env) typs;
begin
match Cons.kind c with
| T.Def (tbs,_) ->
| T.Def (tbs,_)
| T.Newtype (tbs,_) ->
check_con env c;
check_typ_bounds env tbs typs no_region
| T.Abs (tbs, _) ->
Expand Down Expand Up @@ -288,7 +289,7 @@ and check_con env c =
else
begin
env.seen := T.ConSet.add c !(env.seen);
let T.Abs (binds,typ) | T.Def (binds, typ) = Cons.kind c in
let T.Abs (binds,typ) | T.Def (binds, typ) | T.Newtype (binds, typ) = Cons.kind c in
check env no_region (not (T.is_mut typ)) "type constructor RHS is_mut";
let cs, ce = check_typ_binds env binds in
let ts = List.map (fun c -> T.Con (c, [])) cs in
Expand Down
2 changes: 2 additions & 0 deletions src/ir_passes/async.ml
Original file line number Diff line number Diff line change
Expand Up @@ -221,6 +221,8 @@ let transform prog =
Abs (t_binds typ_binds, t_typ typ)
| Def (typ_binds,typ) ->
Def (t_binds typ_binds, t_typ typ)
| Newtype (typ_binds,typ) ->
Newtype (t_binds typ_binds, t_typ typ)

and t_con c =
match Cons.kind c with
Expand Down
2 changes: 2 additions & 0 deletions src/ir_passes/erase_typ_field.ml
Original file line number Diff line number Diff line change
Expand Up @@ -68,6 +68,8 @@ let transform prog =
T.Abs (t_binds typ_binds, t_typ typ)
| T.Def (typ_binds,typ) ->
T.Def (t_binds typ_binds, t_typ typ)
| T.Newtype (typ_binds,typ) ->
T.Newtype (t_binds typ_binds, t_typ typ)

and t_con c =
match Cons.kind c with
Expand Down
4 changes: 4 additions & 0 deletions src/js/astjs.ml
Original file line number Diff line number Diff line change
Expand Up @@ -550,6 +550,10 @@ module Make (Cfg : Config) = struct
to_js_object "TypD"
([ id x ] @ List.map typ_bind_js tp @ [ syntax_typ_js t ]
|> Array.of_list)
| NewtypeD (x, tp, t) ->
to_js_object "NewtypeD"
([ id x ] @ List.map typ_bind_js tp @ [ syntax_typ_js t ]
|> Array.of_list)
| ClassD (eo, sp, s, x, tp, p, rt, i, dfs) ->
to_js_object "ClassD"
(parenthetical eo
Expand Down
31 changes: 30 additions & 1 deletion src/lowering/desugar.ml
Original file line number Diff line number Diff line change
Expand Up @@ -121,6 +121,8 @@ and exp' at note = function
(blob_dotE x.it (exp e)).it
| S.DotE (e, x, _) when T.is_prim T.Text e.note.S.note_typ ->
(text_dotE x.it (exp e)).it
| S.DotE (e, x, _) when x.it = "unwrap" && T.is_con e.note.S.note_typ -> (* TODO: the kind changed to Def in this T.Con, extract `is_newtype` function and document this *)
(exp e).it (* Newtype .unwrap is identity *)
| S.DotE (e, x, _) ->
begin match T.as_obj_sub [x.it] e.note.S.note_typ with
| T.Actor, _ -> I.PrimE (I.ActorDotPrim x.it, [exp e])
Expand Down Expand Up @@ -616,7 +618,7 @@ and export_runtime_information self_id =
[{ it = I.{ name = lab; var = v }; at = no_region; note = typ }])

and build_stabs (df : S.dec_field) : stab option list = match df.it.S.dec.it with
| S.TypD _ -> []
| S.TypD _ | S.NewtypeD _ -> []
| S.MixinD _ -> assert false
| S.IncludeD(_, arg, note) ->
(* TODO: This is ugly. It would be a lot nicer if we didn't have to split
Expand Down Expand Up @@ -998,6 +1000,33 @@ and dec' d =
end
| S.VarD (i, e) -> [I.VarD (i.it, e.note.S.note_typ, exp e)]
| S.TypD _ -> []
| S.NewtypeD (id, binds, _) ->
let c = Option.get id.note in
let tbs_closed, t_body_closed = match Cons.kind c with
| T.Newtype (tbs, t) ->
(* Mutate Newtype kind to Def so downstream IR/codegen sees a transparent alias *)
Cons.unsafe_set_kind c (T.Def (tbs, t));
tbs, t
| _ -> assert false
in
(* Build polymorphic identity function type for the newtype constructor *)
let tbs' = typ_binds binds in
let vars = List.map (fun (tb : I.typ_bind) -> T.Con (tb.it.I.con, [])) tbs' in
let inner_t = T.open_ vars t_body_closed in
let newtype_ret = T.Con (c, vars) in
let type_var_args = List.mapi (fun i tb -> T.Var (tb.T.var, i)) tbs_closed in
let ctor_typ = T.Func (T.Local, T.Returns, tbs_closed, [t_body_closed], [T.Con (c, type_var_args)]) in
(* Build identity function binding for the newtype constructor *)
let arg_var = fresh_var "x" inner_t in
let arg = { it = id_of_var arg_var; at = no_region; note = inner_t } in
let ctor_body = varE arg_var in
let ctor_func =
{ it = I.FuncE (id.it, T.Local, T.Returns, tbs', [arg], [newtype_ret], ctor_body);
at = no_region;
note = Note.{ def with typ = ctor_typ } }
in
let ctor_pat = { it = I.VarP id.it; at = no_region; note = ctor_typ } in
[I.LetD (ctor_pat, ctor_func)]
| S.MixinD _ -> []
| S.IncludeD(_, args, note) ->
let { imports = is; pat = p; decs } = Option.get !note in
Expand Down
2 changes: 2 additions & 0 deletions src/mo_def/arrange.ml
Original file line number Diff line number Diff line change
Expand Up @@ -284,6 +284,8 @@ module Make (Cfg : Config) = struct
| VarD (x, e) -> "VarD" $$ [id x; exp e]
| TypD (x, tp, t) ->
"TypD" $$ [id x] @ List.map typ_bind tp @ [typ t]
| NewtypeD (x, tp, t) ->
"NewtypeD" $$ [id x] @ List.map typ_bind tp @ [typ t]
| ClassD (eo, sp, s, x, tp, p, rt, i, dfs) ->
"ClassD" $$
parenthetical eo
Expand Down
1 change: 1 addition & 0 deletions src/mo_def/syntax.ml
Original file line number Diff line number Diff line change
Expand Up @@ -259,6 +259,7 @@ and dec' =
| LetD of pat * exp * exp option (* immutable, with an optional fail block *)
| VarD of id * exp (* mutable *)
| TypD of typ_id * typ_bind list * typ (* type *)
| NewtypeD of typ_id * typ_bind list * typ (* newtype *)
| ClassD of (* class *)
exp option * sort_pat * obj_sort * typ_id * typ_bind list * pat * typ option * id * dec_field list
| MixinD of pat * dec_field list (* mixin *)
Expand Down
2 changes: 2 additions & 0 deletions src/mo_frontend/bi_match.ml
Original file line number Diff line number Diff line change
Expand Up @@ -296,6 +296,8 @@ let bi_match_typs ctx =
bi_match_typ rel eq inst any (open_ ts1 t) t2
| _, Def (tbs, t) -> (* TBR this may fail to terminate *)
bi_match_typ rel eq inst any t1 (open_ ts2 t)
| Newtype _, Newtype _ when Cons.eq con1 con2 ->
bi_match_list bi_equate_typ rel eq inst any ts1 ts2
| _ when Cons.eq con1 con2 ->
assert (ts1 = []);
assert (ts2 = []);
Expand Down
2 changes: 1 addition & 1 deletion src/mo_frontend/definedness.ml
Original file line number Diff line number Diff line change
Expand Up @@ -184,7 +184,7 @@ and dec msgs d = match d.it with
| LetD (p, e, None) -> pat msgs p +++ exp msgs e
| LetD (p, e, Some f) -> pat msgs p +++ exp msgs e +++ exp msgs f
| VarD (i, e) -> (M.empty, S.singleton i.it) +++ exp msgs e
| TypD (i, tp, t) -> (M.empty, S.empty)
| TypD (i, tp, t) | NewtypeD (i, tp, t) -> (M.empty, S.empty)
| ClassD (eo, csp, s, i, tp, p, t, i', dfs) ->
((M.empty, S.singleton i.it) +++
(* TBR: treatment of eo *)
Expand Down
2 changes: 1 addition & 1 deletion src/mo_frontend/effect.ml
Original file line number Diff line number Diff line change
Expand Up @@ -147,7 +147,7 @@ and infer_effect_dec dec =
| LetD (_, e, None)
| VarD (_, e) ->
effect_exp e
| TypD _
| TypD _ | NewtypeD _
| ClassD _
| MixinD _
| IncludeD _ ->
Expand Down
1 change: 1 addition & 0 deletions src/mo_frontend/error_reporting.ml
Original file line number Diff line number Diff line change
Expand Up @@ -138,4 +138,5 @@ let terminal2token (type a) (symbol : a terminal) : token =
| T_WRAPMULASSIGN -> WRAPMULASSIGN
| T_WRAPPOWASSIGN -> WRAPPOWASSIGN
| T_PIPE -> PIPE
| T_NEWTYPE -> NEWTYPE
| T_WEAK -> WEAK
4 changes: 3 additions & 1 deletion src/mo_frontend/parser.mly
Original file line number Diff line number Diff line change
Expand Up @@ -225,7 +225,7 @@ and objblock eo s id ty dec_fields =
%token AWAIT AWAITSTAR AWAITQUEST ASYNC ASYNCSTAR BREAK CASE CATCH CONTINUE DO LABEL DEBUG
%token IF IGNORE IN IMPLICIT ELSE SWITCH LOOP WHILE FOR RETURN TRY THROW FINALLY WITH
%token ARROW ASSIGN
%token FUNC TYPE OBJECT ACTOR CLASS PUBLIC PRIVATE SHARED SYSTEM QUERY
%token FUNC TYPE NEWTYPE OBJECT ACTOR CLASS PUBLIC PRIVATE SHARED SYSTEM QUERY
%token SEMICOLON SEMICOLON_EOL COMMA COLON SUB DOT QUEST BANG
%token AND OR NOT
%token IMPORT INCLUDE MODULE MIXIN
Expand Down Expand Up @@ -963,6 +963,8 @@ dec_nonvar :
LetD (p', e', None) @? at $sloc }
| TYPE x=typ_id tps=type_typ_params_opt EQ t=typ
{ TypD(x, tps, t) @? at $sloc }
| NEWTYPE x=typ_id tps=type_typ_params_opt EQ t=typ
{ NewtypeD(x, tps, t) @? at $sloc }
| sp=shared_pat_opt FUNC
xf_tps_p=func_pat t=annot_opt fb=func_body
{ (* This is a hack to support local func declarations that return a computed async.
Expand Down
1 change: 1 addition & 0 deletions src/mo_frontend/printers.ml
Original file line number Diff line number Diff line change
Expand Up @@ -168,6 +168,7 @@ let repr_of_symbol : xsymbol -> (string * string) =
| X (T T_ADDOP) -> unop "+"
| X (T T_ACTOR) -> simple_token "actor"
| X (T T_PIPE) -> simple_token "|>"
| X (T T_NEWTYPE) -> simple_token "newtype"
| X (T T_WEAK) -> simple_token "weak"
(* non-terminals *)
| X (N N_bl) -> "<bl>", "<bl>"
Expand Down
1 change: 1 addition & 0 deletions src/mo_frontend/source_lexer.mll
Original file line number Diff line number Diff line change
Expand Up @@ -256,6 +256,7 @@ rule token mode = parse
| "throw" { THROW }
| "to_candid" { TO_CANDID }
| "true" { BOOL true }
| "newtype" { NEWTYPE }
| "type" { TYPE }
| "var" { VAR }
| "weak" { WEAK }
Expand Down
3 changes: 3 additions & 0 deletions src/mo_frontend/source_token.ml
Original file line number Diff line number Diff line change
Expand Up @@ -125,6 +125,7 @@ type token =
| PRIM
| PIPE
| UNDERSCORE
| NEWTYPE
| WEAK
| COMPOSITE
(* Trivia *)
Expand Down Expand Up @@ -261,6 +262,7 @@ let to_parser_token :
| UNDERSCORE -> Ok Parser.UNDERSCORE
| COMPOSITE -> Ok Parser.COMPOSITE
| PIPE -> Ok Parser.PIPE
| NEWTYPE -> Ok Parser.NEWTYPE
| WEAK -> Ok Parser.WEAK
(*Trivia *)
| SINGLESPACE -> Error (Space 1)
Expand Down Expand Up @@ -399,6 +401,7 @@ let string_of_parser_token = function
| Parser.UNDERSCORE -> "UNDERSCORE"
| Parser.COMPOSITE -> "COMPOSITE"
| Parser.PIPE -> "PIPE"
| Parser.NEWTYPE -> "NEWTYPE"
| Parser.WEAK -> "WEAK"

let is_lineless_trivia : token -> void trivia option = function
Expand Down
2 changes: 1 addition & 1 deletion src/mo_frontend/static.ml
Original file line number Diff line number Diff line change
Expand Up @@ -98,7 +98,7 @@ and exp_fields m efs = List.iter (fun (ef : exp_field) ->
exp m ef.it.exp) efs

and dec m d = match d.it with
| TypD _ | ClassD _ | MixinD _ -> ()
| TypD _ | NewtypeD _ | ClassD _ | MixinD _ -> ()
| ExpD e -> exp m e
| LetD (p, e, fail) -> pat m p; exp m e; Option.iter (exp m) fail
| VarD _ | IncludeD _ -> err m d.at
Expand Down
2 changes: 1 addition & 1 deletion src/mo_frontend/traversals.ml
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,7 @@ let rec over_exp (f : exp -> exp) (exp : exp) : exp = match exp.it with
f { exp with it = IgnoreE (over_exp f exp1)}

and over_dec (f : exp -> exp) (d : dec) : dec = match d.it with
| TypD _ -> d
| TypD _ | NewtypeD _ -> d
| ExpD e -> { d with it = ExpD (over_exp f e)}
| VarD (x, e) ->
{ d with it = VarD (x, over_exp f e)}
Expand Down
Loading
Loading