enso/docs/syntax/types.md

layout	title	category	tags	order
developer-doc	Types and Type Signatures	syntax	syntax types	7

Types and Type Signatures

Enso is a statically typed language, meaning that every variable is associated with information about the possible values it can take. In Enso, the type language is the same as the term language, with no artificial separation. For more information on the type system, please see the types design document.

This section will refer to terminology that has not been defined in this document. This is as this document is a specification rather than a guide, and it is expected that you have read the above-linked document on the type-system design as well.

Additionally, this document will colloquially refer to the left and right hand sides of the type ascription operator : as the 'term' and 'type' levels, respectively. In reality, there is no separation between the two in Enso, but it is a useful way of thinking about things when discussing type signatures.

• Type Signatures
  • Type Operators
  • Typeset Literals
  • Writing Type Signatures
  • Behaviour of Type Signatures
• Operations on Types
• Type Definitions
  • Body Atom Definitions
  • Visibility and Access Modifiers

Type Signatures

Enso allows users to provide explicit type signatures for values through use of the type ascription operator :. The expression a : b says that the value a has the type b attributed to it.

foo : (m : Monoid) -> m.this

Type signatures in Enso have some special syntax:

• The reserved name in is used to specify the monadic context in which a value resides. The Enso expression a in IO is equivalent to the Haskell MonadIO a.

  foo : Int -> Int in IO
  

• The operator ! is used to specify the potential for an error value in a type. The expression a ! E says that the type is either an a or an error value of type E.

  / : Number -> Number -> Number ! ArithError
  

Type Operators

Please note that :, in, and ! all behave as standard operators in Enso. This means that you can section them, which is incredibly useful for programming with types. In addition, Enso supports a number of additional operators for working with types. These are listed below.

Operator	Precedence Relations	Level	Assoc.	Description
:	> =	0	Left	Ascribes the type (the right operand) to the value of the left operand.
in	> :, > !	3	Left	Ascribes the context (the right operand) to the value of the left operand.
!	> :, > ->	2	Left	Combines the left operand with the right operand as an error value.
->	> :	1	Left	Represents a mapping from the left operand to the right operand (function).
<:	> !, < |, > in	4	Left	Asserts that the left operand is structurally subsumed by the right.
~	== <:	4	Left	Asserts that the left and right operands are structurally equal.
;	< :, > =	-2	Left	Concatenates the left and right operand typesets to create a new typeset.
|	> <:, > !, > in, > :	5	Left	Computes the union of the left and right operand typesets.
&	> |	6	Left	Computes the intersection of the left and right operand typesets.
:=	< :, > =, > ;	-1	Left	Creates a typeset member by assigning a value to a label.

Solving this set of inequalities produces the relative precedence levels for these operators shown in the table above. In order to check this, you can use the following formula as an input to an SMTLib compatible solver. For reference, bind (=) has a relative level of -3 in this ordering.

(declare-fun ascrip () Int)   ; `:`
(declare-fun bind () Int)     ; `=`
(declare-fun in () Int)       ; `in`
(declare-fun err () Int)      ; `!`
(declare-fun fn () Int)       ; `->`
(declare-fun sub () Int)      ; `<:`
(declare-fun eq () Int)       ; `~`
(declare-fun tsConcat () Int) ; `;`
(declare-fun tsUnion () Int)  ; `|`
(declare-fun tsInter () Int)  ; `&`
(declare-fun tsMember () Int) ; `:=`

(assert (> ascrip bind))
(assert (> in ascrip))
(assert (> in err))
(assert (> err ascrip))
(assert (> err fn))
(assert (> fn ascrip))
(assert (> sub err))
(assert (< sub tsUnion))
(assert (> sub in))
(assert (= eq sub))
(assert (< tsConcat ascrip))
(assert (> tsConcat bind))
(assert (> tsUnion sub))
(assert (> tsUnion err))
(assert (> tsUnion in))
(assert (> tsUnion ascrip))
(assert (> tsInter tsUnion))
(assert (> minus tsInter))
(assert (< tsMember ascrip))
(assert (> tsMember bind))
(assert (> tsMember tsConcat))

(check-sat)
(get-model)
(exit)

A permalink to the program using an online Z3 console can be found here.

The actionables for this section are:

• Decide which of these should be exposed in the surface syntax.

Typeset Literals

Sometimes it is useful or necessary to write a typeset literal in your code. These work as follows.

• Typeset Member: Syntax for typeset members have three components:

  • Label: The name of the member. This must always be present.
  • Type: The type of the member. This need not be present.
  • Value: A value for the member. This need not be present.

  This looks like the following:

  label : Type := value
  

  Please note that the right-hand-side of the := operator is not a pattern context.

• Member Concatenation: Members can be combined into a typeset using the concatenation operator ;.

  x ; y
  

• Typeset Literals: A typeset literal consists of zero or more typeset member definitions concatenated while surrounded by curly braces {}. The braces are necessary as they delimit a pattern context to allow the introduction of new identifiers.

  { x: T ; y: Q }
  

Typeset literals are considered to be a pattern context, and hence the standard rules apply.

Writing Type Signatures

When ascribing a type to a value, there are two main ways in which it can be done. Both of these ways are semantically equivalent, and ascribe the type given by the signature (to the right of the :) to the expression to the left of the :.

1. Inline Ascription: Using the type ascription operator to associate a type signature with an arbitrary expression.

   my_expr : Type
   

2. Freestanding Ascription: Using the type ascription operator to associate a type with a name. The name must be defined on the line below the ascription.

   a : Type
   a = ...
   

3. Binding Ascription: Using the type ascription operator to associate a type with a binding at the binding site.

   a : Type = ... # this is equivalent to the above example
   
   (a : Type) -> ... # use in a lambda
   

The actionables for this section are:

• In the future do we want to support freestanding ascription that isn't directly adjacent to the ascribed value?

Behaviour of Type Signatures

In Enso, a type signature operates to constrain the values that a given variable can hold. Type signatures are always checked, but Enso may maintain more specific information in the type inference and checking engines about the type of a variable. This means that:

• Enso will infer constraints on types that you haven't necessarily written.
• Type signatures can act as a sanity check in that you can encode your intention as a type.
• If the value is of a known type (distinguished from a dynamic type), constraints will be introduced on that type.
• Where the type of the value is known, ascription can be used to constrain that type further.
• It is legal to add constraints to an identifier using : in any scope in which the identifier is visible.

From a syntactic perspective, the type ascription operator : has the following properties:

• The right hand operand to the operator introduces a pattern context.
• The right hand side may declare fresh variables that occur in that scope.
• It is not possible to ascribe a type to an identifier without also assigning to that identifier.
• Introduced identifiers will always shadow other identifiers in scope due to the fact that : introduces a new scope on its RHS.
• Constraint implication is purely feed-forward. The expression b:A only introduces constraints to b.

The actionables for this section are:

• How do signatures interact with function bodies in regards to scoping?
• Does this differ for root and non-root definitions?

Operations on Types

Enso also provides a set of rich operations on its underlying type-system notion of typesets. Their syntax is as follows:

• Union - |: The resultant typeset may contain a value of the union of its arguments.
• Intersection - &: The resultant typeset may contain values that are members of both its arguments.

The actionables for this section are:

• Unify this with the types document at some point. The types document supersedes this section while this actionable exists.

Type Definitions

Types in Enso are defined by using the type reserved name. This works in a context-dependent manner that is discussed properly in the type system design document, but is summarised briefly below.

• Body with Atom Definitions: If you provide a body with atom definitions, this defines a smart constructor that defines the atoms and related functions by returning a typeset.

  type Maybe
      Nothing
      Just (value : Integer)
  
      is_just self = case self of
          Maybe.Nothing -> False
          Maybe.Just _ -> True
  
      nothing self = self.is_just.not
  

  To reference atoms use type name followed by the name of the atom. E.g. Maybe.Nothing or Maybe.Just 2. Atom constructors act like functions and fully support currying - e.g. one can create fn = Maybe.Just and later apply two to it (fn 2) to obtain new atom.

• Autoscoped Constructors: Referencing constructors via their type name may lead to long and boilerplate code. To simplify referencing constructors when the context is known a special .. syntax is supported. Should there be a method describe:

  describe (m : Maybe) -> Text = if m.is_just then m.value.to_text else "Empty"
  

  one may invoke it as describe (Maybe.Just 5) - e.g. the regular way. Or one may use autoscoped constructors and call

  describe (..Just 5)
  

  the argument (..Just 5) is recorded but not executed until it is send to the describe method. The argument of the describe method is known to be of type Maybe and have Just constructor. The scope is now known and the so far deferred .. value gets evaluated. Maybe.Just 5 atom is constructed and execution of describe method continues with such atom.

• Body Without Atom Definitions: If you provide a body and do not define any atoms within it, this creates an interface that asserts no atoms as part of it.

  type HasName
  name: String
  

In addition, users may write explicit this constraints in a type definition, using the standard type-ascription syntax:

type Semigroup
    <> : this -> this

type Monoid
    this : Semigroup
    use Nothing

Body Atom Definitions

When defining an atom in the body of a type (as described above), there are two ways in which you can define an atom:

1. Create a New Atom: Using the type keyword inside the body of a type will define a new atom with the fields you specify. The syntax for doing this is the same as that of a bare atom.

type Just value

2. Include an Atom: You can also use a type body to define methods on an already existing atom. To do this, you can include the atom in the type's body by naming it explicitly. This will introduce it into the scope of your type and define any methods you define in your type on the included atom.

Nothing

Visibility and Access Modifiers

While we don't usually like making things private in a programming language, it sometimes the case that it is necessary to indicate that certain fields should not be touched (as this might break invariants and such like). To this end, we propose an explicit mechanism for access modification that works as follows:

• We have a set of access modifiers, namely private and unsafe.

• We can place these modifiers before a top-level definition.

  type MyAtomType
      type MyAtom a
  
      is_foo : Boolean
      is_foo = ...
  
      private private_method a b = ...
  
      unsafe unsafe_method a b = ...
  

• By default, accessing any member under an access modifier is an error when performed from another module.

• To use members protected by an access modifier, you must import that access modifier from the file in which you want to access those elements.

  import private Base.Data.Vector
  import unsafe Base.Data.Atom
  

• These modified imports are available in all scopes, so it is possible to limit the scope in which you have access to the modified definitions.

  function_using_modifiers v x =
      import private Base.Data.Vector
      import unsafe Base.Data.Atom
  
      v.mutate_at_index 0 (_ -> x)
      x = MyAtom.mutate_field name="sum" (with = x -> x + 20)
      x + 20
  

While private works as you might expect, coming from other languages, the unsafe annotation has additional restrictions:

• It must be explicitly imported from Base.Unsafe.
• When you use unsafe, you must write a documentation comment on its usage that contains a section Safety that describes why this usage of unsafe is valid.