Локальные переменные могут быть объявлены при помощи конструкции let-in , которая вводит новую инициализированную переменную (после lef локальную область видимости(после in). Значение констукции это значение жтого выражения.

let a=3 in a+1 возвращает 4

Если мы хотим определить тип ,то мы можем также написать:

let a:Int = 3 in a+1

Конструкция let-in может быть поределена в терминах базисных fun - выражений.

let a:T = M in N = (fun(a:T)N)(M)

2.3 Базовые типы ,структурные типы и рекурсия.

Типизированное Х-исчисление обычно расширяется разными базовыми типами и структурными типами. В качестве базовых типов мы будем использовать:

Unitпростейший тип из одного элементв ()

Boolс операцией if-then-else

Intc арифметическими операциями и операциями сравнения

Realс арифметическими операциями и операциями сравнения

Stringконкатенация строк

Структурные типы могут быть построены из базовых типов с помощью конструкторов типов. Конструкторы типов в нашем языке включают в себя однонаправленное отношение (->) ,Декартово произведение (*) , записи , универсальный тип.Пара это элемент типа декартово произведение.

value p= 3;true : Int*Bool

Операци над парами это селекторы первого и второго элемента:

fst(p) возвращает 3 snd(p) возвращает true

Записи это неупорядоченное множество именованных переменных. Тип записи можно определить указывая тип , ассоциированный с каждым полем. Тип запись определяется последовательностью именнованных типов ,разделенных запятой и заключенными в фигурные скобки.

Type ARecordType = {a:Int ; b:Bool,c:String }

Запись такого типа может быть создана инициализированием полей записи значениями требуемых типов. Это записано как полседовательность именованных значений разделенных запятыми и заключенные в фигурные скобки.

value r: ARecordType = {a=3;b=true;c="asd"}

Эти поля должны быть уникальными внутри каждой записи. Единственная операция над записями это выбор поля , определяется указанием после точки имя поля.

r.b вызвращает true.

Так как функции это первостепенные значения , записи в общем случае могут иметь компоненты-функции.

Type FunctionRecordType = {f1:Int -> Int : Real -> Real } Value functionRecord = {f1=succ , f2 = sin }

Тип запись может быть определена с помощью существующих типов записей и оператора & ,который является оператором конкатенации двух записей.

Type NewFuctionRecordType = FunctionRecordType & {f3:Bool - > Bool}

Это считается хорошим сокращением , вместо того ,чтобы писать поля f1 ,f2 ,f3 явно.Это работает только , если в записи не будет дубликатных полей.

Структура данных может быть сделана локальной и private в наборе функций объявлением let-in. Записи с компонентами функциями в частности удобный способ для достижения этого. В примере private переменная counter совместно используется функциями increment и total.

value counter = let counter = ref(0)

int {increment = fun(n:Int) count : = count + n , total = fun() count

}

counter.increment(3)

counter.total()возвращает 3.

Этот пример включает сторонние эффекты , клавное пользо приватных переменных это возможномть приватно их обновлять. Примитив ref возвращает ссылку на объект с возможностью обновления и присвоения ограниченно работают на таких ссылках.Эта общая форма сокрытия информации ,которая позволяет обновлять локальное состояние статическую область видимости для ограничения видимости.

Универсальный тип это некоторая форма неупорядоченного множества именнованных типов , которые заключены в квадратные скобки. Элементы этого типа могут быть Integer , Boolean или String.

value v1=[a=3] value v2=[b=true]

value v3=[c="asd"]

Единственная операция на универсальном типе case-выбор.Case-выражение для универсального типа AVariantType имеет следующую форму.

Case variant of

[a=variableof type Int] действие в случае а [b=variableof type Bool] действие в случае b

[c=variableof type String] действие в случае c

где в каждом случае воодится новая переменная и связывается с соответствующим содержимым варианта.Например ниже приведенная функция определенному элементу типа AVariantType возвращает строку

value f = fun (х: AVariantType) case х of

[а = anlnt] "it is an integer

[b = а В oo I] "it is a boolean"

[c = aString] "it is the string:" Л aString otherwise "emor"

где вариантная переменная х может быть связана с идентификаторами abInt ,aBool, aString в зависимости от случая.

В нетипизированном Х-исчислении возможно выражать рекурсивные операторы и использовать их ,чтобы выражать рекурсивные функции. Однако все вычисления выразимые в Х-исчислении должны завершаться. грубо говоря , тип обычно более сложен чем тип её результата ,так как после некотрого числа применений функции мы получаем базовый тип; более того у нас нет незавершенных примитивов). Следовательно рекурсивные определения вводятся как новая концепция примитивов. Функция факториао может быть выражена так:

гес value fact =

fun (n:lnt) if n=0 then 1 else n T fact(n-1)

Для простоты мы предпологаем ,что значения, которые могут быть рекурсивно

определены это только функции.Но в конце концов мы вводим рекурсивное

оперделение типов. Это позволяет нам ,например, определять тип целочисленных

списков без использования записей или универсальных типов.

гес type IntList = [nil: U nit,

cons: {head: Int, tail: IntList}

]

Целочисленный список это либо пустой список ,либо соединение целого числа и целочисленного списка.

2. Типы это множества значений

Какое понятие типа наиболее адекватно , то есть могло бы содержать полиморфиз ,абстракцию и параметризацию? В предудыщих секциях мы начали описывать ччастную систему типов ,предоставляя неформальные правила типизирования для лингвистических конструкций ,которые мы использовали.Этих правил достаточно , чтобы описать систему типов на интуитивном уровне , и могут быть легко формалтзованы как система вывода типов.

Хотя нам необязательно обсуждать семантическую теорию типов подробно ,но может быть полезным изучит некоторые базовые правила.Эти правила в свою очередь полезны для понимания правил типизирования ,в частности касаясь концепции выделения подтипов ,которая будет ввелена позже.

Есть множество V всех значений , содержащее простые значения такие как integer , структуры данных ,например пары, записи и универсалные типы и функции.Это законченное упорядовачение ,построенное техникой Скотта[Scott, 76], но в первом своем приближении мы можем подумать ,что это просто большое множество всех вычислимых типов.