From e7d1aa58f764651fc676c95b23f43457b1b91dfa Mon Sep 17 00:00:00 2001 From: aarne Date: Fri, 27 Jun 2008 11:21:49 +0000 Subject: removed obsolete items from doc --- doc/transfer-reference.html | 842 -------------------------------------------- 1 file changed, 842 deletions(-) delete mode 100644 doc/transfer-reference.html (limited to 'doc/transfer-reference.html') diff --git a/doc/transfer-reference.html b/doc/transfer-reference.html deleted file mode 100644 index d858b1c06..000000000 --- a/doc/transfer-reference.html +++ /dev/null @@ -1,842 +0,0 @@ - - - - - -Transfer language reference - -

Transfer language reference

- -Author: Björn Bringert <bringert@cs.chalmers.se>
-Last update: Wed Mar 1 13:52:22 2006 -
- -

-
-

- - -

-
-

-

-WARNING: The Transfer language is still experimental. Its syntax, type system and semantics may change without notice. I will try to help you with any problems this might cause, but I will not refrain from changing the language solely for reasons of backwards compatibility. -

-

-This document describes the features of the Transfer language. -See the Transfer tutorial -for an example of a Transfer program, and how to compile and use -Transfer programs. -

-

-Transfer is a dependently typed functional programming language -with eager evaluation. The language supports generalized algebraic -datatypes, pattern matching and function overloading. -

- -

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 overloaded -functions must be given explicitly, not as metavariables. -

- -

Layout syntax

-

-Transfer uses layout syntax, where the indentation of a piece of code -determines which syntactic block it belongs to. -

-

-To give the block structure without using layout -syntax, you can enclose the block in curly braces and -separate the parts of the blocks with semicolons. -

-

-For example, this case expression: -

-
-  case x of
-         p1 -> e1
-         p2 -> e2
-
-

-

-is equivalent to this one: -

-
-  case x of {
-         p1 -> e1 ;
-         p2 -> e2 
-  }
-
-

-

-Here the layout is insignificant, as the structure is given with -braces and semicolons. Thus it is equivalent to: -

-
-  case x of { p1 -> e1 ; p2 -> e2 }
-
-

- -

Imports

-

-A Transfer module starts with some imports. Most modules will have to -import the prelude, which contains definitons used by most programs: -

-
-  import prelude
-
-

-

-For more information about the standard prelude, see Standard prelude. -

- -

Function declarations

-

-Functions need to be given a type and a definition. The type is given -by a typing judgement on the form: -

-
-  f : T
-
-

-

-where f is the function's name, and T its type. See -Function types for a how the types of functions -are written. -

-

-The definition of the function is then given as a sequence of pattern -equations. The first equation whose patterns match the function arguments -is used when the function is called. Pattern equations are on the form: -

-
-  f p11 ... p1m = exp1
-  ...
-  f pn1 ... pnm = expn
-
-

-

-where p11 to pnm are patterns, see Patterns. -

-

-Pattern equations can also have guards, boolean expressions which determine -whether to use the equation when the pattern has been matched. Pattern equations -with guards are written: -

-
-  f p11 ... p1m | guard1 = exp1
-  ...
-  f pn1 ... pnm | guardn = expn
-
-

-

-Pattern equations with and without guards can be mixed in the definiton of -a function. -

-

-Any variables bound in the patterns are in scope in the guards and -right hand sides of each pattern equation. -

- -

Data type declarations

-

-Transfer supports Generalized Algebraic Datatypes. -They are declared thusly: -

-
-  data D : T where 
-       c1 : Tc1
-       ...
-       cn : Tcn
-
-

-

-Here D is the name of the data type, T is the type of the type -constructor, c1 to cn are the data constructor names, and -Tc1 to Tcn are their types. -

-

-FIXME: explain the constraints on the types of type and data constructors. -

- -

Lambda expressions

-

-Lambda expressions are terms which express functions, without -giving names to them. For example: -

-
-  \x -> x + 1
-
-

-

-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: -

-
-  let x1 = exp1
-      ...
-      xn = expn
-   in exp
-
-

-

-Here, the variables x1 to xn are in scope in all the expressions -exp1 to expn, and in exp. Thus let-defined functions can be -mutually recursive. -

- -

Types

- -

Function types

-

-Functions types are of the form: -

-
-  A -> B
-
-

-

-This is the type of functions which take an argument of type -A and returns a result of type B. -

-

-To write functions which take more than one argument, we use currying. -A function which takes n arguments is a function which takes one -argument and returns a function which takes n-1 arguments. Thus, -

-
-  A -> (B -> C)
-
-

-

-or, equivalently, since -> associates to the right: -

-
-  A -> B -> C
-
-

-

-is the type of functions which take teo arguments, the first of type -A and the second of type B. This arrangement lets us do -partial application of function to fewer arguments than the function -is declared to take, returning a new function which takes the rest -of the arguments. -

-

Dependent function types

-

-In a function type, the value of an argument can be used later -in the type. Such dependent function types are written: -

-
-  (x : A) -> B
-
-

-

-Here, x is in scope in B. -

- -

Basic types

-

Integers

-

-The type of integers is called Integer. -Standard decmial integer literals, such as 0 and 1234 are used to -represent values of this type. -

-

Floating-point numbers

-

-The only currently supported floating-point type is Double, which supports -IEEE-754 double-precision floating-point numbers. Double literals are written -in decimal notation, e.g. 123.456. -

-

Strings

-

-There is a primitive String type. String literals are written -with double quotes, e.g. "this is a string". -FIXME: This might be replaced by a list of -characters representation in the future. -

-

Booleans

-

-Booleans are not a built-in type, though some features of the Transfer language -depend on them. The Bool type is defined in the -Standard prelude. -

-
-  data Bool : Type where
-          True : Bool
-          False : Bool
-
-

-

-In addition to normal pattern matching on booleans, you can use the built-in -if-expression: -

-
-  if exp1 then exp2 else exp3
-
-

-

-where exp1 must be an expression of type Bool. -

- -

Records

-

Record types

-

-Record types are created by using a sig expression: -

-
-  sig { l1 : T1; ... ; ln : Tn }
-
-

-

-Here, l1 to ln are the field labels and T1 to Tn are field types. -

-

Record values

-

-Record values are constructed using rec expressions: -

-
-  rec { l1 = exp1; ... ; ln = expn }
-
-

-

Record projection

-

-Fields are selected from records using the . operator. This expression selects -the field l from the record value r: -

-
-  r.l
-
-

-

Records and layout syntax

-

-The curly braces and semicolons are simply explicit layout syntax, so -the record type and record expression above can also be written as: -

-
-  sig l1 : T1
-      ...
-      ln : Tn
-
-

-
-  rec l1 = exp1
-      ...
-      ln = expn
-
-

- -

Record subtyping

-

-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: -

-
-  (exp1, ..., expn)
-
-

-

-are syntactic sugar for records with fields p1 to pn. The expression -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. -The list type is declared as: -

-
-  data List : Type -> Type where 
-          Nil : (A:Type) -> List A
-          Cons : (A:Type) -> A -> List A -> List A
-
-

-

-The empty list can be written as []. There is an operator :: which can -be used instead of Cons. These are just syntactic sugar for expressions -using Nil and Cons, with the type arguments hidden. -

- -

Case expressions

-

-Pattern matching is done in pattern equations and with the -case construct: -

-
-  case exp of
-       p1 | guard1 -> rhs1
-       ...
-       pn | guardn -> rhsn
-
-

-

-where p1 to pn are patterns, see Patterns. -guard1 to guardn are boolean expressions. Case arms can also be written -without guards, such as: -

-
-       pk -> rhsk
-
-

-

-This is the same as writing: -

-
-       pk | True -> rhsk
-
-

- -

Patterns

- -

Constructor patterns

-

-Constructor patterns are written as: -

-
-  C p1 ... pn
-
-

-

-where C is a data constructor which takes n arguments. -If the value to be matched is C v1 ... vn, -then v1 to vn will be matched against p1 to pn. -

- -

Variable patterns

-

-A variable pattern is a single identifier: -

-
-  x
-
-

-

-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. -Note that variable patterns may not use the same identifier as data constructors -which are in scope, since they will then be interpreted as constructor -patterns. -

- -

Wildcard patterns

-

-Wildcard patterns are written with a single underscore: -

-
-  _
-
-

-

-Wildcard patterns match all values and bind no variables. -

- -

Record patterns

-

-Record patterns match record values: -

-
-  rec { l1 = p1; ... ; ln = pn }
-
-

-

-A record value matches a record pattern if the record value has all the -fields l1 to ln, and their values match p1 to pn. -

-

-Note that a record value may have more fields than the record pattern. -The values of these fields do not influence the pattern matching. -

- -

Disjunctive patterns

-

-It is possible to write a pattern on the form: -

-
-  p1 || ... || pn
-
-

-

-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

-

-When pattern matching on lists, there are two special constructs. -A whole list can by matched be a list of patterns: -

-
-  [p1, ... , pn]
-
-

-

-This pattern will match lists of length n, such that each element -in the list matches the corresponding pattern. The empty list pattern: -

-
-  []
-
-

-

-is a special case of this. It matches the empty list, oddly enough. -

-

-Non-empty lists can also be matched with ::-patterns: -

-
-  p1::p2
-
-

-

-This pattern matches non-empty lists such that the first element of -the list matches p1 and the rest of the list matches p2. -

- -

Tuple patterns

-

-Tuples patterns on the form: -

-
-  (p1, ... , pn)
-
-

-

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

- -

String literal patterns

-

-String literals can be used as patterns. -

- -

Integer literal patterns

-

-Integer literals can be used as patterns. -

- -

Metavariables

-

-Metavariables are written as questions marks: -

-
-  ?
-
-

-

-A metavariable is a way to tell the 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 -and dictionary arguments explicitly. -

- -

Overloaded functions

-

-In Transfer, functions can be overloaded by having them take a record -of functions as an argument. For example, the functions for equality -and inequality in the Transfer Prelude are defined as: -

-
-  Eq : Type -> Type
-  Eq A = sig eq : A -> A -> Bool
-  
-  eq : (A : Type) -> Eq A -> A -> A -> Bool
-  eq _ d = d.eq
-  
-  neq : (A : Type) -> Eq A -> A -> A -> Bool
-  neq A d x y = not (eq A d x y)
-
-

-

-We call Eq a type class, though it's actually just a record type -used to pass function implementations to overloaded functions. We -call a value of type Eq A an Eq dictionary for the type A. -The dictionary is used to look up the version of some function for the -particular type we want to use the function on. Thus, in order to use -the eq function on two integers, we need a dictionary of type -Eq Integer: -

-
-  eq_Integer : Eq Integer
-  eq_Integer = rec eq = prim_eq_Integer
-
-

-

-where prim_eq_Integer is the built-in equality function for -integers. To check whether two numbers x and y are equal, we -can then call the overloaded eq function with the dictionary: -

-
-  eq Integer eq_Integer x y
-
-

-

-Giving the type at which to use the overloaded function, and the appropriate -dictionary can be cumbersome. Metavariables come to the rescue: -

-
-  eq ? ? x y
-
-

-

-The type checker can in most cases figure out the values of the type and -dictionary arguments. NOTE: this is not implemented yet. -

- -

Type class extension

-

-By using record subtyping, see Record subtyping, we can -create type classes which extend other type classes. A dictionary for the -new type class can also be used as a dictionary for old type class. -

-

-For example, we can extend the Eq type class above to Ord, a type -class for orderings: -

-
-  Ord : Type -> Type
-  Ord A = sig eq : A -> A -> Bool
-              compare : A -> A -> Ordering
-
-

-

-To extend an existing class, we keep the fields of the class we want to -extend, and add any new fields that we want. Because of record subtyping, -for any type A, a value of type Ord A is also a value of type Eq A. -

- -

Extending multiple classes

-

-A type class can also extend several classes, by simply having all the fields -from all the classes we want to extend. The Num class in the -Standard prelude is an example of this. -

- -

Standard prelude

-

-The standard prelude, see prelude.tra, -contains definitions of a number of standard types, functions and -type classes. -

- -

Operators

-

-Most built-in operators in the Transfer language are translated -to calls to overloaded functions. This means that they can be -used at any type for which there is a dictionary for the type class -in question. -

- -

Unary operators

- - - - - - - - - - - -
OperatorPrecedenceTranslation
-10-x => negate ? ? x
- -

- -

Binary operators

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
OperatorPrecedenceAssociativityTranslation of x op y
>>=3leftbind ? ? x y
>>3leftbind ? ? x (\_ -> y)
||4rightif x then True else y
&&5rightif x then y else False
==6noneeq ? ? x y
/=6noneneq ? ? x y
<6nonelt ? ? x y
<=6nonele ? ? x y
>6nonegt ? ? x y
>=6nonege ? ? x y
::7rightCons ? ? x y
+8leftplus ? ? x y
-8leftminus ? ? x y
*9lefttimes ? ? x y
/9leftdiv ? ? x y
%9leftmod ? ? x y
- -

- -

Compositional functions

- -

do notation

-

-Sequences of operations in the Monad type class can be written -using do-notation, like in Haskell: -

-
-  do x <- f
-     y <- g x
-     h y
-
-

-

-is equivalent to: -

-
-  f >>= \x -> g x >>= \y -> h y
-
- - - - -- cgit v1.2.3