ShotDs.Data.Type (shot_ds v1.0.0)

Copy Markdown View Source

Provides a data structure for Church's simple types.

Examples

iex> o = Type.new(:o)
%ShotDs.Data.Type{goal: :o, args: []}

iex> io = Type.new(:o, :i)
%ShotDs.Data.Type{goal: :o, args: [%ShotDs.Data.Type{goal: :i, args: []}]}

iex> Type.new(io, [o, :o])
%ShotDs.Data.Type{
  goal: :o,
  args: [
    %ShotDs.Data.Type{goal: :i, args: []},
    %ShotDs.Data.Type{goal: :o, args: []},
    %ShotDs.Data.Type{goal: :o, args: []}
  ]
}

Summary

Types

t()

The type of a simple type.

type_id()

The type of a basic type.

Functions

fresh_type_var()

Creates a fresh variable for a simple type using Erlang references.

new(goal, args \\ [])

Creates a new simple type. Optionally, a list of arguments can be specified.

type_var?(type)

Checks whether the given type or type identifier is a type variable.

Types

t()

@type t() :: %ShotDs.Data.Type{args: [t()], goal: type_id()}

The type of a simple type.

The goal can be a concrete name for the type like :i or :o or a reference denoting a type variable. The arguments of a type are a list of simple types.

Note that this is an uncurried representation of higher-order types.

type_id()

@type type_id() :: atom() | reference()

The type of a basic type.

A basic type is identified as an atom (concrete type) or a reference (type variable).

Functions

fresh_type_var()

@spec fresh_type_var() :: t()

Creates a fresh variable for a simple type using Erlang references.

new(goal, args \\ [])

@spec new(type_id() | t(), type_id() | t() | [type_id() | t()]) :: t()

Creates a new simple type. Optionally, a list of arguments can be specified.

Behaves as identity function on a single argument representing a simple type.

type_var?(type)

@spec type_var?(t() | type_id()) :: boolean()

Checks whether the given type or type identifier is a type variable.