ShotDs.Data.Context (shot_ds v1.2.0)

Represents a type environment for parsing and type checking. Can also be created by using the ~e sigil from ShotDs.Hol.Sigils.

Constants are stored as ShotDs.Data.TypeScheme, enabling rank-1 polymorphism: each lookup of a constant via get_type/2 produces a fresh instantiation of its scheme. Constants declared with a bare monotype are wrapped in a trivial scheme and behave identically to a monomorphic declaration.

Term variables are always stored as monotypes as Hindley-Milner only enables generalization in let-bindings, not in lambda-abstractions.

Examples

iex> Context.new()
%ShotDs.Data.Context{vars: %{}, consts: %{}}

iex> Context.new() |> Context.put_var("X", Type.new(:o))
%ShotDs.Data.Context{
  vars: %{"X" => %ShotDs.Data.Type{goal: :o, args: []}},
  consts: %{}
}

Summary

Types

t()

The type of the type environment.

Functions

get_const_scheme(ctx, name)

Returns the scheme of the constant with the given name, or nil if it is not bound. Unlike get_type/2, this does not instantiate; callers that need the raw scheme should use this function.

get_type(ctx, name)

Returns the type of the given name. For variables, the stored monotype is returned. For constants, the stored scheme is instantiated producing a fresh monotype with new type variables for each quantified parameter.

new()

Creates an empty context.

put_const(ctx, name, type_or_scheme)

Associates the constant with the given name with the given type or scheme. Bare monotypes are wrapped in a trivial scheme. Overwrites the old value if present.

put_var(ctx, name, type)

Associates the variable with the given name with the given type in the context. Overwrites the old value if present.

Types

t()

@type t() :: %ShotDs.Data.Context{
  consts: %{required(String.t()) => ShotDs.Data.TypeScheme.t()},
  type_vars: %{required(String.t()) => reference()},
  vars: %{required(String.t()) => ShotDs.Data.Type.t()}
}

The type of the type environment.

A context contains the type of variables (:vars) as a Map from its name to its type. Likewise for the constants (:consts). The type constraints are represented as a MapSet of ShotDs.Data.Type pairs.

The type_vars field maps TH1 type-variable names to their reference() identifiers for use during formula-level polymorphism parsing.

Functions

get_const_scheme(ctx, name)

@spec get_const_scheme(t(), String.t() | reference()) ::
  ShotDs.Data.TypeScheme.t() | nil

Returns the scheme of the constant with the given name, or nil if it is not bound. Unlike get_type/2, this does not instantiate; callers that need the raw scheme should use this function.

get_type(ctx, name)

@spec get_type(t(), String.t()) :: ShotDs.Data.Type.t() | nil

Variables shadow constants of the same name. Returns nil if the name is not bound.

Note

Each call for a polymorphic constant returns a different monotype with disjoint fresh type variables.

new()

@spec new() :: t()

Creates an empty context.

put_const(ctx, name, type_or_scheme)

@spec put_const(
  t(),
  String.t() | reference(),
  ShotDs.Data.Type.t() | ShotDs.Data.TypeScheme.t()
) :: t()

Associates the constant with the given name with the given type or scheme. Bare monotypes are wrapped in a trivial scheme. Overwrites the old value if present.

put_var(ctx, name, type)

@spec put_var(t(), String.t() | reference(), ShotDs.Data.Type.t()) :: t()

Associates the variable with the given name with the given type in the context. Overwrites the old value if present.