From 141fa43eb88c0a646a9631ff9dddff5261b379cd Mon Sep 17 00:00:00 2001 From: bringert Date: Wed, 7 Dec 2005 09:46:21 +0000 Subject: [PATCH] Transfer reference: added metavariable section and implementation status section. --- doc/transfer-reference.html | 133 ++++++++++++++++++++++-------------- doc/transfer-reference.txt | 32 +++++++-- 2 files changed, 105 insertions(+), 60 deletions(-) diff --git a/doc/transfer-reference.html b/doc/transfer-reference.html index d96269db5..820f0f152 100644 --- a/doc/transfer-reference.html +++ b/doc/transfer-reference.html @@ -7,44 +7,45 @@

Transfer language reference

Author: Björn Bringert <bringert@cs.chalmers.se>
-Last update: Tue Dec 6 14:26:07 2005 +Last update: Wed Dec 7 10:45:42 2005

@@ -61,6 +62,16 @@ Transfer is a dependently typed functional programming language with eager evaluation.

+

Current implementation status

+

+Not all features of the Transfer language have been implemented yet. The most +important missing piece is the type checker. This means that there are almost +no checks done on Transfer programs before they are run. It also means that +the values of metavariables are not inferred. Thus metavariables cannot +be used where their values matter. For example, dictionaries for overlaoded +functions must be given explicitly, not as metavariables. +

+

Layout syntax

Transfer uses layout syntax, where the indentation of a piece of code @@ -98,7 +109,7 @@ braces and semicolons. Thus the above is equivalent to: case x of { p1 -> e1 ; p2 -> e2 }

- +

Imports

A Transfer module start with some imports. Most modules will have to @@ -108,7 +119,7 @@ import the prelude, which contains definitons used by most programs: import prelude

- +

Function declarations

Functions need to be given a type and a definition. The type is given @@ -134,7 +145,7 @@ is used when the function is called. Pattern equations are on the form: f qn1 ... qnm = exp

- +

Data type declarations

Transfer supports Generalized Algebraic Datatypes. @@ -152,7 +163,7 @@ Here D is the name of the data type, T is the type of constructor, c1 to cn are the data constructor names, and Tc1 to Tcn are their types.

- +

Lambda expressions

Lambda expressions are terms which express functions, without @@ -166,7 +177,7 @@ giving names to them. For example: is the function which takes an argument, and returns the value of the argument + 1.

- +

Local definitions

To give local definition to some names, use: @@ -178,7 +189,7 @@ To give local definition to some names, use: in exp

- +

Types

Function types

@@ -229,7 +240,7 @@ in the type. Such dependent function types are written: Here, x1 can be used in T2 to Tn, x1 can be used in T2 to Tn

- +

Basic types

Integers

@@ -270,7 +281,7 @@ if-expression:

where exp1 must be an expression of type Bool.

- +

Records

Record types are created by using a sig expression: @@ -309,7 +320,7 @@ A record of some type R1 can be used as a record of any type R2 such that for every field p1 : T1 in R2, p1 : T1 is also a field of T1.

- +

Tuples

Tuples on the form: @@ -326,7 +337,7 @@ above is equivalent to: rec { p1 = exp1; ... ; pn = expn }

- +

Lists

The List type is not built-in, though there is some special syntax for it. @@ -343,7 +354,7 @@ The empty lists can be written as []. There is a operator ::< be used instead of Cons. These are just syntactic sugar for expressions using Nil and Cons, with the type arguments hidden.

- +

Pattern matching

Pattern matching is done in pattern equations and by using the @@ -374,7 +385,7 @@ This is the same as writing:

The syntax of patterns are decribed below.

- +

Constructor patterns

Constructor patterns are written as: @@ -389,7 +400,7 @@ If the value to be matched is the constructor C applied to arguments v1 to vn, then v1 to vn will be matched against p1 to pn.

- +

Variable patterns

A variable pattern is a single identifier: @@ -402,7 +413,7 @@ A variable pattern is a single identifier: A variable pattern matches any value, and binds the variable name to the value. A variable may not occur more than once in a pattern.

- +

Wildcard patterns

Wildcard patterns are written as with a single underscore: @@ -414,7 +425,7 @@ Wildcard patterns are written as with a single underscore:

Wildcard patterns match all values and bind no variables.

- +

Record patterns

Record patterns match record values: @@ -431,7 +442,7 @@ fields l1 to ln, and their values match p1 - +

Disjunctive patterns

It is possible to write a pattern on the form: @@ -444,9 +455,9 @@ It is possible to write a pattern on the form: A value will match this pattern if it matches any of the patterns p1 to pn. FIXME: talk about how this is expanded

- -

List patterns

+

List patterns

+

Tuple patterns

Tuples patterns on the form: @@ -458,27 +469,43 @@ Tuples patterns on the form:

are syntactic sugar for record patterns, in the same way as tuple expressions.

- +

String literal patterns

String literals can be used as patterns.

- +

Integer literal patterns

Integer literals can be used as patterns.

- -

Meta variables

-

Type classes

+

Metavariables

+

+Metavariable are written as questions marks: +

+
+  ?
+
+

+

+A metavariable is a way to the the Transfer type checker that: +"you should be able to figure out what this should be, +I can't be bothered to tell you". +

+

+Metavariables can be used to avoid having to give type variables +and dictionaries explicitly. +

-

Operators

+

Overloaded functions / Type classes

-

Compositional functions

+

Operators

+

Compositional functions

+

do notation

- + diff --git a/doc/transfer-reference.txt b/doc/transfer-reference.txt index dd16e2d39..a7d534363 100644 --- a/doc/transfer-reference.txt +++ b/doc/transfer-reference.txt @@ -2,7 +2,6 @@ Transfer language reference Author: Björn Bringert Last update: %%date(%c) - % NOTE: this is a txt2tags file. % Create an html file from this file using: % txt2tags transfer.txt @@ -11,10 +10,6 @@ Last update: %%date(%c) %!options(html): --toc - - - - This document describes the features of the Transfer language. See the [Transfer tutorial transfer-tutorial.html] for an example of a Transfer program, and how to compile and use @@ -23,6 +18,16 @@ Transfer programs. Transfer is a dependently typed functional programming language with eager evaluation. +== Current implementation status == + +**Not all features of the Transfer language have been implemented yet**. The most +important missing piece is the type checker. This means that there are almost +no checks done on Transfer programs before they are run. It also means that +the values of metavariables are not inferred. Thus metavariables cannot +be used where their values matter. For example, dictionaries for overlaoded +functions must be given explicitly, not as metavariables. + + == Layout syntax== Transfer uses layout syntax, where the indentation of a piece of code @@ -401,9 +406,22 @@ String literals can be used as patterns. Integer literals can be used as patterns. -== Meta variables == +== Metavariables == -== Type classes == +Metavariable are written as questions marks: + +``` +? +``` + +A metavariable is a way to the the Transfer type checker that: +"you should be able to figure out what this should be, +I can't be bothered to tell you". + +Metavariables can be used to avoid having to give type variables +and dictionaries explicitly. + +== Overloaded functions / Type classes == == Operators ==