An Advanced Type System for Gerbil v0.19 #1504

New issue

vyzo · 2026-09-19T10:51:29Z

vyzo commented

2026-09-19 10:51:29 +00:00

An advanced type system for Gerbil v0.19

Extending binding forms for types

The expander already supports type attachment to runtime bindings; we should use this machinery and make expansion aware of types so that we no longer have to use using for something that the expander can infer.
All top level bindings can have a type, and we should have custom typed expansion for things like let so that the type can be derived from the declaration. No complicated type inference algorithm is required, just use the annotatations and the type of expression procedures.

so we have something like this:

(defclass A ((x : X)))

(def (foo x)
  (let (a (A x))
    a.x))

(def global-a ... : A)

(def (bar ...)
  global-a.x)

this should work without requiring a using incantation.

We can also extend let to accept type annotation sigils, at which point using becomes completely hidden from typical user programs.
This is also critical for generic type constructions.

(let (a expr : A)
  a.x)

Type Constructors and Macros

We need syntactic support for constructing types and macros at the type level.
We can define the builtin type constructors by extending deftype:

(deftype (Type-constructor arg ...)
  type-construction-expression)

We can define macros for types with constructs like defsyntax-for-type, deftype-rule and deftype-rules.
These define macros that expand at type resolution time.
Derived type constructors can be defined as type macros.

Union Types

We need to support union types for otherwise disjoint types, not just homogeneous types.
Let's define a (U type ...) constructor for union types, which must have a representation supported by the compiler.

For instance, a union betwen a string and a list for psettings passed in things like call-with-input-file:

(U :string :list)

Parameteric Types

Type Erasure at runtime

let's not carry higher order types in the runtime; the runtime should only preserve
low level, MOP-mapped types for efficiency and dynamic compatibility.

So each higher order type should have a concrete runtime type.

Parametric Procedure Types

We need to make procedures higher order typed, with concrete type :procedure.
Let's say we introduce a procedure type constructor

(Procedure return-type required-argument-type ...
  [#!optional optional-argument-type ...]
  [#!key keyword-spec ...]
  [#!optional keyword-spec ...]
  [#!rest tail-type])
return-type : type
keyword-spec: keyword type

For instance:

assoc :: (Procedure (Maybe :pair) :t :list)

Parameteric container types

builtin things like :pair, :list, :vector, :values, :box, :promise, :parameter should get type parameter(s).

Pairs and Homogeneous Lists

List can be a derived type from Pair and :null:

(Pair type-of-car type-of-cdr)
(List homogeneous-element-type) = (U :null (Pair homogeneous-element-type (List homogeneous-element-type)))

Pairs have concrete type :pair and lists have concrete type :list.

Homogeneous Vectors

The homogeneous vector type:

(Vector element-type)
(Vector element-type fixed-size)

Values

Values is a variadic type describing how many values it contains and their types:

(Values value-type ...)

(Values type) is equivalent to type.

Box

the parameter restricts the type of the box value

(Box type)

(box x) => (Box (type-of x))

Promise

The type is implied by the return type of the procedure it contains.

(Promise return-type)

Parameter

The type parameter restricts the parameterization type.

(Parameter type)

Generics

This is where things get more interesting: we can introduce generic type parameter syntax, so that we can have procedures and types that generalize over parameters.

Let's define a syntax first: i propose reusing the {} method notation for generic types (reader macro wraps with @method).

So we can have generic type constructors for all parameteric types; here is how a generic procedure definition would look like:

(def {?k ?v} (assoc (el : ?k) (lst : (AList ?k ?v))) => (Pair ?k ?v) ...)

and here is syntax for defining a generic class and a generic interface:

(defclass {?t} A ((a : ?t)))
(defclass {?t} (B (A ?t)) ((b : ?t)))

(interface {?t ?r} I
  (foo (a : ?t) => ?r)

Constructing this object would require a type annotation to declare the concrete type since this cannot be generally inferred.
Let's say we generalize the HashTable interface to specify key and value types:

(interface {?k ?v} HashTable
  (ref {?d} (k : ?k) (default : ?d)) => (U ?v ?d)
  (set! (k : ?k) (v : ?v)) => :void
  (for-each (proc : (Procedure :t ?k ?v))) => :void
  ...)

But hash tables are still constructed by make-hash-table, which has no way of seeing the concrete type.
So we can declare this as:

(let (ht (make-hash-table) : (HashTable :symbol :t)) ...)

This may be problematic however so maybe we need special syntax for specifying the generic arguments.
We can consider this:

(make-hash-table {:symbol :t} arg ...)

but there is a conflict with dynamic method dispatch and applicative order of evaluation.
A heavy handed solution would be to use wrapper generic instantiation:

(template {:symbol :t} (make-hash-table arg ...)

We can make this more palatable with a shortcut unicode notation sigil:

(τ {:symbol :t} (make-hash-table arg ...))

with the semantics being apply template construction to the operator of the s-expression.

Omitting the template constructor for a procedure for which the template cannot be inferred by the arguments
would leave all the template parameters as :t.

Variadic Signatures

we can type a variadic procedure with its definition, reusing the ellipsis token:

(def (foo (a : A) (b : B) ...)
  ...)

where b is the variadic argument list in the body, and an implicit contract check is installed at call sites.
This can also make apply type safe.

As an alternative, we can also use the :: token:

(def (foo (a : A) :: (b : B))
  ...)

this is compatible with the list constructor signature.

No Monomorphization

In general monomorphization results in high compile times and code bloat; it is also somewhat incompatible
with the dynamic nature of Gerbil, so it is out of scope for v0.19. We can consider it as an optimization for v1.0.

Dependent Types

The :~ contract annotation system already provides a path to express dependent types; the compiler will
have to understand those contracts so that it can propagate them to the point of usage.
For instance, the builtin vector-ref could be defined with a range contract and the compiler should see
this dependent type and eliminate all runtime checks in a properly range checked loop and emit the unchecked
##vector-ref. Same for string-ref, builtin homogeneous numeric vectors, and so on.

In general, once the compiler understands contract dependent types we
should never have to write a ## primitive for vector/string/etc
access; the compiler should do it automagically.

Revisiting Procedure Signatures

If we want to support dependent types on procedure signatures and perform reduction at call site we need
to carry the full contracts and optional defaults in the procedure signature; that also means we can validate
the dependent contract at call site and reduce to the unchecked variant of the procedure; closures can be automatically
reduced to their unchecked variant when they are passed to a properly typed receiver.

So how would signatures look? We need to have a form that names arguments so that dependent types can work.
I propose we use the [] reader macro (@list) for writing named arguments

I think we should have this general form:

(Procedure [{generic-type-variable ...}]
  return-type
  required-argument-spec ...
  [#!optional optional-argument-spec ...]
  [#!key keyword-argument-spec ...]
  [#!optional optional-keyword-argument-spec ...]
  [#!rest variadic-argument-type])

required-argument-spec:
 | type
 | \[name type\]

optional-argument-spec:
 | type
 | \[name type default-value‌\]

keyword-argument-spec
 | keyword type
 | keyword [name type]

optional-keyword-argument-spec
 | keyword type
 | \[keyword name type\]

# An advanced type system for Gerbil v0.19 ## Extending binding forms for types The expander already supports type attachment to runtime bindings; we should use this machinery and make expansion aware of types so that we no longer have to use `using` for something that the expander can infer. All top level bindings can have a type, and we should have custom typed expansion for things like let so that the type can be derived from the declaration. No complicated type inference algorithm is required, just use the annotatations and the type of expression procedures. so we have something like this: ``` (defclass A ((x : X))) (def (foo x) (let (a (A x)) a.x)) (def global-a ... : A) (def (bar ...) global-a.x) ``` this should work without requiring a `using` incantation. We can also extend let to accept type annotation sigils, at which point `using` becomes completely hidden from typical user programs. This is also critical for generic type constructions. ``` (let (a expr : A) a.x) ``` ## Type Constructors and Macros We need syntactic support for constructing types and macros at the type level. We can define the builtin type constructors by extending deftype: ``` (deftype (Type-constructor arg ...) type-construction-expression) ``` We can define macros for types with constructs like `defsyntax-for-type`, `deftype-rule` and `deftype-rules`. These define macros that expand at type resolution time. Derived type constructors can be defined as type macros. ## Union Types We need to support union types for otherwise disjoint types, not just homogeneous types. Let's define a `(U type ...)` constructor for union types, which must have a representation supported by the compiler. For instance, a union betwen a string and a list for psettings passed in things like `call-with-input-file`: ``` (U :string :list) ``` ## Parameteric Types ### Type Erasure at runtime let's not carry higher order types in the runtime; the runtime should only preserve low level, MOP-mapped types for efficiency and dynamic compatibility. So each higher order type should have a concrete runtime type. ### Parametric Procedure Types We need to make procedures higher order typed, with concrete type `:procedure`. Let's say we introduce a procedure type constructor ``` (Procedure return-type required-argument-type ... [#!optional optional-argument-type ...] [#!key keyword-spec ...] [#!optional keyword-spec ...] [#!rest tail-type]) return-type : type keyword-spec: keyword type ``` For instance: ``` assoc :: (Procedure (Maybe :pair) :t :list) ``` ### Parameteric container types builtin things like `:pair`, `:list`, `:vector`, `:values`, `:box`, `:promise`, `:parameter` should get type parameter(s). #### Pairs and Homogeneous Lists List can be a derived type from `Pair` and `:null`: ``` (Pair type-of-car type-of-cdr) (List homogeneous-element-type) = (U :null (Pair homogeneous-element-type (List homogeneous-element-type))) ``` Pairs have concrete type `:pair` and lists have concrete type `:list`. #### Homogeneous Vectors The homogeneous vector type: ``` (Vector element-type) (Vector element-type fixed-size) ``` #### Values Values is a variadic type describing how many values it contains and their types: ``` (Values value-type ...) ``` `(Values type)` is equivalent to `type`. #### Box the parameter restricts the type of the box value ``` (Box type) (box x) => (Box (type-of x)) ``` #### Promise The type is implied by the return type of the procedure it contains. ``` (Promise return-type) ``` #### Parameter The type parameter restricts the parameterization type. ``` (Parameter type) ``` ## Generics This is where things get more interesting: we can introduce generic type parameter syntax, so that we can have procedures and types that generalize over parameters. Let's define a syntax first: i propose reusing the `{}` method notation for generic types (reader macro wraps with `@method`). So we can have generic type constructors for all parameteric types; here is how a generic procedure definition would look like: ``` (def {?k ?v} (assoc (el : ?k) (lst : (AList ?k ?v))) => (Pair ?k ?v) ...) ``` and here is syntax for defining a generic class and a generic interface: ``` (defclass {?t} A ((a : ?t))) (defclass {?t} (B (A ?t)) ((b : ?t))) (interface {?t ?r} I (foo (a : ?t) => ?r) ``` Constructing this object would require a type annotation to declare the concrete type since this cannot be generally inferred. Let's say we generalize the `HashTable` interface to specify key and value types: ``` (interface {?k ?v} HashTable (ref {?d} (k : ?k) (default : ?d)) => (U ?v ?d) (set! (k : ?k) (v : ?v)) => :void (for-each (proc : (Procedure :t ?k ?v))) => :void ...) ``` But hash tables are still constructed by make-hash-table, which has no way of seeing the concrete type. So we can declare this as: ``` (let (ht (make-hash-table) : (HashTable :symbol :t)) ...) ``` This may be problematic however so maybe we need special syntax for specifying the generic arguments. We can consider this: ``` (make-hash-table {:symbol :t} arg ...) ``` but there is a conflict with dynamic method dispatch and applicative order of evaluation. A heavy handed solution would be to use wrapper generic instantiation: ``` (template {:symbol :t} (make-hash-table arg ...) ``` We can make this more palatable with a shortcut unicode notation sigil: ``` (τ {:symbol :t} (make-hash-table arg ...)) ``` with the semantics being apply template construction to the operator of the s-expression. Omitting the template constructor for a procedure for which the template cannot be inferred by the arguments would leave all the template parameters as :t. ### Variadic Signatures we can type a variadic procedure with its definition, reusing the ellipsis token: ``` (def (foo (a : A) (b : B) ...) ...) ``` where `b` is the variadic argument list in the body, and an implicit contract check is installed at call sites. This can also make `apply` type safe. As an alternative, we can also use the `::` token: ``` (def (foo (a : A) :: (b : B)) ...) ``` this is compatible with the list constructor signature. ### No Monomorphization In general monomorphization results in high compile times and code bloat; it is also somewhat incompatible with the dynamic nature of Gerbil, so it is out of scope for v0.19. We can consider it as an optimization for v1.0. ## Dependent Types The `:~` contract annotation system already provides a path to express dependent types; the compiler will have to understand those contracts so that it can propagate them to the point of usage. For instance, the builtin `vector-ref` could be defined with a range contract and the compiler should see this dependent type and eliminate all runtime checks in a properly range checked loop and emit the unchecked `##vector-ref`. Same for `string-ref`, builtin homogeneous numeric vectors, and so on. In general, once the compiler understands contract dependent types we should never have to write a `##` primitive for vector/string/etc access; the compiler should do it automagically. ### Revisiting Procedure Signatures If we want to support dependent types on procedure signatures and perform reduction at call site we need to carry the full contracts and optional defaults in the procedure signature; that also means we can validate the dependent contract at call site and reduce to the unchecked variant of the procedure; closures can be automatically reduced to their unchecked variant when they are passed to a properly typed receiver. So how would signatures look? We need to have a form that names arguments so that dependent types can work. I propose we use the `[]` reader macro (`@list`) for writing named arguments I think we should have this general form: ``` (Procedure [{generic-type-variable ...}] return-type required-argument-spec ... [#!optional optional-argument-spec ...] [#!key keyword-argument-spec ...] [#!optional optional-keyword-argument-spec ...] [#!rest variadic-argument-type]) required-argument-spec: | type | \[name type\] optional-argument-spec: | type | \[name type default-value‌\] keyword-argument-spec | keyword type | keyword [name type] optional-keyword-argument-spec | keyword type | \[keyword name type\] ```

vyzo commented

2026-09-19 18:12:00 +00:00

made some updates for consistency.

vyzo commented

2026-09-21 10:08:06 +00:00

I think the procedure higher order types should have the full signature, that simplifies dependent types with predicate contracts and does not introduce yet another syntactic construct.

vyzo commented

2026-09-21 10:08:51 +00:00

I think for the first increment we can skip generics -- even push it after v0.19 so that we keep the work bounded.

vyzo commented

2026-09-21 11:28:39 +00:00

I made the proposal more concrete.

vyzo commented

2026-09-21 11:28:52 +00:00

Towards an Advanced Type System for Gerbil v0.19

Objective:

simplify syntax for accessing objects by adding limited type inference to the expander
support higher order types for statically typed procedures and builtin container types
support unions, dependent types and the requisit runtime check elimination.

Simplify syntax for accessing objects

Right now accessing object slots requires either a type signature at procedure level
or a using form. Local bindings, with let forms do not carry the requisite type
information for syntactically accessing slots without a using form.

This can be resolved in two parts:

definitions can can already carry type information. We should make sure the expansion
emits type signatures attached to definitions.
the expander can introduce new let forms, to replace the originals in the core exports,
such that it infers the type of the binding by the value expression.

there are also two natural syntactic extensions that can simplify things:

add an optional type annotation to top level bindings with def; unnecessary for procedures as
they are already typed and the type can be inferred, useful for values.
add an optional type annotation to let form bindings; this will eliminate most direct uses
of the using macro.

The expander will have to do a limited form of type inference for let bindings that lack an
explicit annotation. This will allow us to use dotted notaion throughout the local scope
without the noise of using blocks.

In addition, deftype can be extended so that it is not limited to type alias, but general
type constructors

Union Types

We already have a limited form of unions with the Maybe pseudotype for nullable values.
We can extend this to introduce a full union type which allows us to express disjoint type signatures.
The general syntax would be:

(U type ...)

which creates an or-like disjuniction of possible types.

Higher Order Procedure and builtin contain types

Currently we type procedures at source level with just :procedure. Similarly for values, pairs,
lists, vectors, boxes, promises. We omit parameters for now as they introduce complexity.
This loses static type information that can help simplify check safety without runtime checks and
also complicates the usage of builtin container types.

The solution to this is to introduce higher order typed builtins. Thus the follwing:

(Procedure <signature> ...)
(Pair car-type cdr-type)
(List element-type)
(Values value-type ...)
(Vector element-type [size))
(Box value-type)
(Promise forced-type)

The semantics are as following.

Procedure Types

The type is the complete signature, with named arguments and contracts.
This allows the return type inference in the expander, and argument contract checks which can be statically eliminated in the compiler.
When a procedure is passed to another procedure as value, the exact type can help the compiler
emit the unchecked version of the procedure if the argument contract can be satisfied statically.

Pair and List Types

Pairs have the car and cdr types attached, and the exact types can be attached.
Homogeneous lists have a single type parameter. There is also an equivalence between pairs
and homogeneous lists with a recursive parameteric type declaration:

(deftype (List ?t)
 (U :null (Pair ?e (List ?e))))

Values

This allows us to automatically type the elements of a multiple return value expression.

Boxes

This allows us to automatically type the value of a box, with appropriate runtime checks and static elimination by the compiler.

Promises

This allows us to automatically type the value of a forced promise; the delay constructions can check the requisite return type
of the expression statically, similarly to how procedure return types are checked.

Dependent Types

By virtue of having the complete contract signature, including predicates, visible to the compiler we can eliminate range checks
and other constraints that we know are satisfied. The compiler can accomplish this with partial abstract evaluation.

The builtin type signatures can be extended so that range checks can be lifted and partially evaluated out (say in a loop that
checks bounds) so that the unchecked operator can be invoked.

For instance let's consisder this hypothetical signature and example:

(defbuiltin vector-ref (v : :vector) (el :~ (in-range 0 (vector-length v))) => :t)

(let* ((v a-vector)
       (l (vector-length v)))
  (let loop ((i 0))
    (when (fx< i l)
      (... (vector-ref v i))
      (loop (fx+ i 1)))))

here the compiler should understand the dependent type range end
eliminate all checks in the vector access in the body of the loop; it
should simply emit ##vector-ref.

Parameteric Type syntax

It would be very useful to have a generic parameteric syntax for
type declarations, much akin to generics in other language, only
without the implicit monomorphization at compile time.

This is simply syntax to aid the type inference and allow us to
precisely type container access; the closest analog is generics in
java, with the associated type erasure.

Here we propose a syntax using the {} reader macro which expands to
@method for declarations. When the signature declaration, be it
procedure signatures, classes, or interfaces, has an {?t ...} specification, it then denotes a parameteric type declaration.

We can also extend the syntax of deftype to create parameteric type constructors.

For procedures, the type parameters are signified as the first argument:

(defbuiltin (vector-ref {?t} (v : (Vector ?t)) (i :~ (in-range 0 (vector-length v)) :- :fixnum) => ?t))

(deftype (AList ?k ?v)
  (List (Pair ?k ?v)))

(def (aget {?k ?v} (k : ?k) (alist : (AList ?k ?v))) => (Maybe ?v)
  ....)

For classes and interfaces the parameters are the first argument, before the declaration had:

(defclass {?t} Value ((v : ?t)))

(interface {?k ?v} HashTable
  (set! (k : ?k) (v : ?v)) => :void
  (ref {?default} (k : ?k) (default : ?default)) => (U ?k ?default)
  ...)

It is not always possible to disambiguate the parameters from arguments to procedures and methods; for instance take the
hash table constructor:

(def (make-hash-table {?k ?v} ...) => (HashTable ?k ?v)
  ...)

Invoking the constructor does not provide any way to infer the actual parameter types; for this i propose a special construct
in application syntax that disambiguates the type parameter using the sigil ▷ as the first argument:

(make-hash-table ▷ {A B} ...)

Putting it altogether

This will require changes both in the core prelude (in :gerbil/core/contract) and the compiler.
The prelude will have to accomodate the syntactic extensions for supporting all this and the
compiler will have to be adjusted to understand the extended type family.

# Towards an Advanced Type System for Gerbil v0.19 Objective: - simplify syntax for accessing objects by adding limited type inference to the expander - support higher order types for statically typed procedures and builtin container types - support unions, dependent types and the requisit runtime check elimination. ## Simplify syntax for accessing objects Right now accessing object slots requires either a type signature at procedure level or a `using` form. Local bindings, with `let` forms do not carry the requisite type information for syntactically accessing slots without a `using` form. This can be resolved in two parts: - definitions can can already carry type information. We should make sure the expansion emits type signatures attached to definitions. - the expander can introduce new let forms, to replace the originals in the core exports, such that it infers the type of the binding by the value expression. there are also two natural syntactic extensions that can simplify things: - add an optional type annotation to top level bindings with def; unnecessary for procedures as they are already typed and the type can be inferred, useful for values. - add an optional type annotation to let form bindings; this will eliminate most direct uses of the `using` macro. The expander will have to do a limited form of type inference for let bindings that lack an explicit annotation. This will allow us to use dotted notaion throughout the local scope without the noise of `using` blocks. In addition, `deftype` can be extended so that it is not limited to type alias, but general _type constructors_ ## Union Types We already have a limited form of unions with the Maybe pseudotype for nullable values. We can extend this to introduce a full union type which allows us to express disjoint type signatures. The general syntax would be: ``` (U type ...) ``` which creates an `or`-like disjuniction of possible types. ## Higher Order Procedure and builtin contain types Currently we type procedures at source level with just `:procedure`. Similarly for values, pairs, lists, vectors, boxes, promises. We omit parameters for now as they introduce complexity. This loses static type information that can help simplify check safety without runtime checks and also complicates the usage of builtin container types. The solution to this is to introduce higher order typed builtins. Thus the follwing: ``` (Procedure <signature> ...) (Pair car-type cdr-type) (List element-type) (Values value-type ...) (Vector element-type [size)) (Box value-type) (Promise forced-type) ``` The semantics are as following. ### Procedure Types The type is the complete signature, with named arguments and contracts. This allows the return type inference in the expander, and argument contract checks which can be statically eliminated in the compiler. When a procedure is passed to another procedure as value, the exact type can help the compiler emit the unchecked version of the procedure if the argument contract can be satisfied statically. ### Pair and List Types Pairs have the car and cdr types attached, and the exact types can be attached. Homogeneous lists have a single type parameter. There is also an equivalence between pairs and homogeneous lists with a recursive parameteric type declaration: ``` (deftype (List ?t) (U :null (Pair ?e (List ?e)))) ``` ### Values This allows us to automatically type the elements of a multiple return value expression. ### Boxes This allows us to automatically type the value of a box, with appropriate runtime checks and static elimination by the compiler. ### Promises This allows us to automatically type the value of a forced promise; the delay constructions can check the requisite return type of the expression statically, similarly to how procedure return types are checked. ## Dependent Types By virtue of having the complete contract signature, including predicates, visible to the compiler we can eliminate range checks and other constraints that we know are satisfied. The compiler can accomplish this with partial abstract evaluation. The builtin type signatures can be extended so that range checks can be lifted and partially evaluated out (say in a loop that checks bounds) so that the unchecked operator can be invoked. For instance let's consisder this hypothetical signature and example: ``` (defbuiltin vector-ref (v : :vector) (el :~ (in-range 0 (vector-length v))) => :t) (let* ((v a-vector) (l (vector-length v))) (let loop ((i 0)) (when (fx< i l) (... (vector-ref v i)) (loop (fx+ i 1))))) ``` here the compiler should understand the dependent type range end eliminate all checks in the vector access in the body of the loop; it should simply emit `##vector-ref`. ## Parameteric Type syntax It would be very useful to have a _generic_ parameteric syntax for type declarations, much akin to generics in other language, only without the implicit monomorphization at compile time. This is simply syntax to aid the type inference and allow us to precisely type container access; the closest analog is generics in java, with the associated type erasure. Here we propose a syntax using the `{}` reader macro which expands to `@method` for declarations. When the signature declaration, be it procedure signatures, classes, or interfaces, has an `{?t ...}` specification, it then denotes a parameteric type declaration. We can also extend the syntax of `deftype` to create parameteric type constructors. For procedures, the type parameters are signified as the first argument: ``` (defbuiltin (vector-ref {?t} (v : (Vector ?t)) (i :~ (in-range 0 (vector-length v)) :- :fixnum) => ?t)) (deftype (AList ?k ?v) (List (Pair ?k ?v))) (def (aget {?k ?v} (k : ?k) (alist : (AList ?k ?v))) => (Maybe ?v) ....) ``` For classes and interfaces the parameters are the first argument, before the declaration had: ``` (defclass {?t} Value ((v : ?t))) (interface {?k ?v} HashTable (set! (k : ?k) (v : ?v)) => :void (ref {?default} (k : ?k) (default : ?default)) => (U ?k ?default) ...) ``` It is not always possible to disambiguate the parameters from arguments to procedures and methods; for instance take the hash table constructor: ``` (def (make-hash-table {?k ?v} ...) => (HashTable ?k ?v) ...) ``` Invoking the constructor does not provide any way to infer the actual parameter types; for this i propose a special construct in application syntax that disambiguates the type parameter using the sigil `▷` as the first argument: ``` (make-hash-table ▷ {A B} ...) ``` ## Putting it altogether This will require changes both in the core prelude (in :gerbil/core/contract) and the compiler. The prelude will have to accomodate the syntactic extensions for supporting all this and the compiler will have to be adjusted to understand the extended type family.

vyzo commented

2026-09-21 14:22:02 +00:00

I started the discussion with astra.

Sign in to join this conversation.