foetus Language  

foetus Syntax  

A foetus program consists of terms and definitions.

P : :

| term; P term to be evaluated

| definition; P definition for further use

When processing input, foetus evaluates the terms and stores the definitions in the environment. ``Reserved words'' in the foetus language are case, of, let and in. Special characterss are ( ) [ ] { } | . , ; = =>. An identifier may contain letters, digits, apostrophies and underscores. If it starts with a small letter it stands for a variable, else it denotes a constant.

Term syntax.

In the following x , x₁ , x₂ , ... denote variables, C , C₁ , C₂ , ... constants and u , t , t₁ , t₂ , ... foetus terms.

t : : x

| [x]t lambda

| tu application

| C(t) constructor

$$\Rightarrow \Rightarrow$$ | pattern matching

| (C₁ = t₁,...,C_n = t_n) tuple

| t.C projection

| let x₁ = t₁,...,x_n = t_n in t let

| (t) (extra parentheses)

Definitions.

A definition statement has the form x₁ = t₁,...,x_n = t_n (it is a let-term without a ``body''). All variables x₁,...,x_n are defined simultanously, thus can refer to each other.

Example.

The following foetus program defines addition on natural numbers (spanned by the two constructors O ``zero'' and S ``successor'') and calculates 1 + 1 .

add = [x][y]case x of 
        { O z => y
        | S x' => S(add x' y) };
one = S(O());
add one one;

Note that although O is a zero-argument-constructor the syntax forces us to supply a dummy variable z within the pattern definition and also empty tuple () in the definition of one.

foetus Type System

In the following x , x₁ , x₂ , ... denote variables, C , C₁ , C₂ , ... constants, u , t , t₁ , t₂ , ... foetus terms, $\tau$ , $\sigma$ , $\sigma_{1}^{}$ , $\sigma_{2}^{}$ , ... foetus types and X , X₁ , X₂,... type variables. $\Gamma$ = x₁ : $\sigma_{1}^{}$,...,x_n : $\sigma_{n}^{}$ denotes the context. The judgement

$$\Gamma$$ $$\vdash$$ t : $$\sigma$$

means ``in context $\Gamma$ term t is of type $\sigma$ ''.

Type formation.

$$\tau \sigma \rightarrow \tau \rightarrow$$ : :

$$\sigma_{1}^{} \sigma_{n}^{}$$ | labeled sum type

$$\sigma_{1}^{} \sigma_{n}^{}$$ | labeled product type

$$\tau$$ | polymorphic type

$$\tau \sigma$$ | instantiation of polymorphic type

$$\sigma_{1}^{} \sigma_{n}^{} \tau$$ | recursive type

In the formation of a recursive type with Let X_i may only appear strict positiv in $\sigma_{i}^{}$ . We define congruence on types $\cong$ as the smallest congruence closed under

Let $$\vec{X}$$ = $$\vec{\sigma}$$ in $$\tau$$ $$\cong$$ $$\tau$$[X₁ : = Let $$\vec{X}$$ = $$\vec{\sigma}$$ in X₁;...;X_n : = Let $$\vec{X}$$ = $$\vec{\sigma}$$ in X_n]

( $\vec{X}$ = $\vec{\sigma}$ abbreviates X₁ = $\sigma_{1}^{}$,...,X_n = $\sigma_{n}^{}$ ). Thus we can substitute congruent types:

$$\ru {\Gamma\vdash t:\sigma \quad \sigma\cong\tau} {\Gamma\vdash t: \tau}$$

For ploymorphic types we have rules like in System F:

$$\rux {\Gamma\vdash t : \sigma \quad \mbox{$X$ not free type variable in $\Gamma$}} {\Gamma\vdash t : \{X\}\sigma} {poly-i}$$

$$\rux {\Gamma\vdash t: \{X\}\sigma} {\Gamma\vdash t: \sigma[X:=\tau]} {poly-e}$$

Typing rules for foetus terms

We here only briefly introduce the typing rules. For more detailed explanation, read a book about type theorie, e.g. [NPS90].

Lambda abstraction.

$$\rux {\Gamma,x:\sigma \vdash t:\tau} {\Gamma\vdash [x]t : \sigma \rightarrow \tau} {\rightarrow-i}$$

Application.

$$\rux {\Gamma\vdash t:\sigma\rightarrow\tau \quad \Gamma\vdash u:\sigma} {\Gamma\vdash t u : \sigma} {\rightarrow-e}$$

Constructor.

$$\rux {\Gamma\vdash t:\sigma_i} {\Gamma\vdash C_i(t) : \{ C_1 : \sigma_1 \vert \dots \vert C_n : \sigma_n \}} {\{\}-i}$$

Pattern matching.

$$\rux {\Gamma\vdash t: \{ C_1 : \sigma_1 \vert \dots \vert C_n : \... ...ghtarrow u_1 \vert \dots \vert C_n(x_n)\Rightarrow u_n \} : \sigma} {\{\}-e}$$

Tupels.

$$\rux {\Gamma\vdash t_i : \sigma_i\ \mbox{for all $1\leq i\leq n$}... ..._1=t_1,\dots,C_n=t_n) : ( C_1 : \sigma_1 , \dots , C_n : \sigma_n )} {()-i}$$

Projection.

$$\rux {\Gamma\vdash t:( C_1 : \sigma_1 , \dots , C_n : \sigma_n )} {\Gamma\vdash t.C_i : \sigma_i} {()-e}$$

Let.

$$\rux {\Gamma,x_1:\sigma_1,\dots,x_n:\sigma_n \vdash t_i : \sigma_... ...\Gamma\vdash \mathrm{let}\ x_1=t_1;\dots ;x_n=t_n\ \mathrm{in}\ u:\tau} {let}$$

In foetus type checking is not yet implemented and it is assummed that all terms entered are well typed. Of course, only for well typed terms the termination check produces valid results.

Example.

The following well-known example for non-termination passes the foetus termination checker, but it is not well typed.

f = [x]x x;
a = f f;

foetus output:

f passes termination check
a passes termination check

Run example.