Dr. Dobb's is part of the Informa Tech Division of Informa PLC

This site is operated by a business or businesses owned by Informa PLC and all copyright resides with them. Informa PLC's registered office is 5 Howick Place, London SW1P 1WG. Registered in England and Wales. Number 8860726.


Channels ▼
RSS

Design

Cat: A Functional Stack-Based Little Language


The Type System

Static type systems are useful for documentation, static verification of code, and optimization. It is common practice in stack languages to document the stack effects of each instruction—what type of values are removed from the stack (the consumption), and what type of values are placed on the stack (the production). The Cat type system allows type annotations (aka "type signatures" or "stack diagrams") that express the effect of an expression in terms of the consumption and production. If a type annotation is omitted, Cat is able to infer a type automatically using a variant of the Hindley-Milner algorithm (research.microsoft.com/Users/luca /Papers/BasicTypechecking.pdf). Example 5 shows some type signatures. From the Cat interpreter, the metacommand #t gives you the type of any function on the stack (metacommands are commands intended for the interpreter and are not part of the language; by convention, they are affixed with a "#" character).

Type variables are denoted with a leading apostrophe ('). Type variable names starting with lowercase letters represent individual types (scalar type variables). Type variable names starting with uppercase letters represent type vectors. A type vector is zero or more types on the stack. A type vector can be left unbound in the type signature of an expression, but ultimately has to be bound to a concrete sequence of types for an expression to be executable. ([apply] apply is not a valid program because we cannot resolve all the type variables.)

The arrow is used to differentiate function types with side effects ('A ~>'B) from those without ('A->'B). The rule for determining whether a function has a side effect is simply whether it uses a function with a side effect.


42 : ( -> int)
+ : (int int -> int)
dup : ('a -> 'a 'a)
pop : ('a -> )
apply : ('A ('A -> 'B) -> 'B)
if : ('A bool ('A -> 'B) ('A -> 'B) -> 'B)
[1 +] : ( -> (int -> int))
quote : ('a -> ( -> 'a))

Example 5: Sample type signatures.

In intermediate languages, it is useful to be able to verify certain properties of code statically. The most important properties are:

  • Whether the inputs of the correct type are available when a function is called.
  • Whether an expression can underflow the stack or not.

To guarantee proper verification of these properties, intermediate languages with stack-based semantics (such as the JVML) usually have a requirement that conditional execution cannot lead to different stack configurations (the types of values on the stack have to agree). The same principle applies to Cat, so the following is illegal:


is_monday ["I hate Mondays"] [42] if

In this case, depending on whether it is Monday, you would have either a string or integer on the top of the stack. This violates the type of the if function, which requires that both arguments ["I hate Mondays"] and [42] yield the same vector of types (denoted by 'B).

A novel feature of the Cat type system is that all functions are row polymorphic. Each function takes an implicit type-vector variable (called a "row variable") as an argument representing the rest of the stack. The row variable is returned implicitly along with the rest of the results. Another nice feature of the Cat type system is that you can perform partial type inference and compute the type of a polymorphic expression without context. This feature is not present in the Hindley-Milner type inference algorithms.


Related Reading


More Insights






Currently we allow the following HTML tags in comments:

Single tags

These tags can be used alone and don't need an ending tag.

<br> Defines a single line break

<hr> Defines a horizontal line

Matching tags

These require an ending tag - e.g. <i>italic text</i>

<a> Defines an anchor

<b> Defines bold text

<big> Defines big text

<blockquote> Defines a long quotation

<caption> Defines a table caption

<cite> Defines a citation

<code> Defines computer code text

<em> Defines emphasized text

<fieldset> Defines a border around elements in a form

<h1> This is heading 1

<h2> This is heading 2

<h3> This is heading 3

<h4> This is heading 4

<h5> This is heading 5

<h6> This is heading 6

<i> Defines italic text

<p> Defines a paragraph

<pre> Defines preformatted text

<q> Defines a short quotation

<samp> Defines sample computer code text

<small> Defines small text

<span> Defines a section in a document

<s> Defines strikethrough text

<strike> Defines strikethrough text

<strong> Defines strong text

<sub> Defines subscripted text

<sup> Defines superscripted text

<u> Defines underlined text

Dr. Dobb's encourages readers to engage in spirited, healthy debate, including taking us to task. However, Dr. Dobb's moderates all comments posted to our site, and reserves the right to modify or remove any content that it determines to be derogatory, offensive, inflammatory, vulgar, irrelevant/off-topic, racist or obvious marketing or spam. Dr. Dobb's further reserves the right to disable the profile of any commenter participating in said activities.

 
Disqus Tips To upload an avatar photo, first complete your Disqus profile. | View the list of supported HTML tags you can use to style comments. | Please read our commenting policy.