Мне было интересно, какой именно тип пустого списка находится в SML (я использую PolyML)? Когда я печатаю [] в интерпретатор, я выберусь:Каков тип пустого списка в ML?
val it = []: 'a list
который я бы ожидать. Но тогда, если бы я был ввести сказать:
fun f a = if a = 0 then [] else [[]];
тогда я получаю:
val f = fn: int -> 'a list list
, которые, казалось бы, подразумевает, что [] имеет тип 'a list list также. Как именно это работает?
В терминологии ML значение имеет схему , а не тип. Типовая схема представляет собой набор типов. Это тип с подстановочными знаками, а подстановочные знаки можно заменить любым типом. Замена подстановочных знаков по типам называется экземпляр типовой схемы.
В 'a list, 'a является переменной типа, то есть подстановочным знаком. Пустой список [] может использоваться в любом типе, который является экземпляром схемы типа 'a list. То есть для любого типа T пустой список имеет тип T list. Например, пустой список имеет тип int list и тип bool list и тип (int * int * int) list и тип int list list и так далее. Все эти типы являются экземплярами типовой схемы 'a list.
Когда переменная встречается несколько раз, ее необходимо последовательно менять. Например, fn x => x (функция идентификации) имеет схему типа 'a -> 'a; он имеет тип int -> int и тип bool -> bool, но не тип int -> bool. Значение с типовой схемой 'a -> 'b будет иметь тип int -> bool.
Значение может иметь несколько типов - это распространенное явление в языках программирования. Это свойство основного языка ML, что набор типов хорошо типизированного значения является точно набором экземпляров схемы типа. Это свойство называется княжество: система типов ML является основной. Конкретные реализации ML, как правило, имеют исключения из княжества; например, SML имеет исключение из-за перегрузки операторов (fn x => x + x имеет два типа: int -> int и float -> float, а правила разрешения перегрузки приводят к тому, что компилятор принимает решение о int -> int, если контекст не налагает float).
Значение, схема основного типа которого содержит по меньшей мере одну переменную, называется polymorphic. Значение, схема основного типа которого не содержит переменных, называется monomorphic.
Подстановочный знак может быть заменен схемой типа. Это дает другую схему типа, которая является подмножеством исходного набора, то есть схема типа представляет собой схему меньшего типа (уточнение) оригинала. Например, значение [[]] имеет типовую схему 'a list list: оно имеет тип T list list для любого типа T.[[]] имеет тип int list list и тип bool list list и тип (int * int * int) list list и т.д.
В литературе о ML, «тип» часто используется как синоним «схемы типа», так что обычно говорят, что «пустой список имеет тип 'a list ". В литературе о системах типов «тип» часто означает, что терминология ML называется «схемой типа», а другие термины, такие как «тип земли», используются для типа без переменных.
Большое спасибо за уточняющую терминологию! –
Является ли ваше замешательство тем, что в конечном типе все еще есть '' a', или у вас будет такая же проблема с 'if a = 0 then [] else [1]', где тип '[]' внезапно становится 'int list'? – sepp2k
Да, я понимаю, что вы имеете в виду - я думаю, что мое замешательство возникло из-за того, что я одновременно просматривал две сигнатуры типа, т. Е. Я ошибочно считал, что «a» в первом типе должен быть таким же, как «a» во втором тип подпись - но все это имеет смысл сейчас, спасибо :). – micromegas