Для n = 0 и n = 1 ответ должен быть ясным (ноль, много).
Но что за n> 1?
TL; DR: Для некоторого n, да, но не в целом.
Позвольте мне понять, если эти ясные ответы:
- n = 0: Нет, нет значений, которые относятся к нулевым типам. (Если значение существует, оно должно иметь тип. Значения не существуют в SML, пока не определен их тип.)
- n = 1: Да, существует значение, которое принадлежит ровно одному типу. (Существует бесконечно много способов, которыми вы можете express значение, принадлежащее ровно одному типу:
datatype one = One, datatype two = One | Two, datatype three = One | Two | Three, и в этом случае любой из этих конструкторов значений принадлежит только одному типу в любой одной точке. )
Если это неправильная интерпретация вашего вопроса, не могли бы вы уточнить и уточнить вопрос и эти четкие ответы? Продолжая предположение, что эта интерпретация верна, вот некоторые соображения для n> 1:
Чтобы значение имело несколько типов, оно должно быть polymorphi c. Я могу придумать два пути:
Для " ad-ho c полиморфизм " (он же перегрузка): n = K: некоторые ограниченные примеры перегрузки, встроенные операторы, которые имеют несколько типов (например, +, имеющие оба типа int * int -> int и real * real -> real, в зависимости от того, к какому выводу это относится.) Я, честно говоря, точно не знаю, сколько типов перегружено для + типов , но я вижу, что это по крайней мере 3:
- 1 + 1;
> val it = 2 : int
- 1.0 + 1.0;
> val it = 2.0 : real
- 0w1 + 0w1;
> val it = 0wx2 : word
Так что для некоторого произвольного K ≥ 3: Да, op + - это значение, которое имеет ровно K типов.
Может быть существует несколько перегруженных встроенных значений с различным количеством типов, но поскольку перегруженных встроенных операторов имеется только конечное число, это может быть верно только для очень немногих n> 1 и не для всех n> 1 в general.
Можно утверждать, что на самом деле это три разных значения op + с одинаковыми именами. Они реализованы по-разному и ведут себя по-разному, поэтому было бы разумно сказать, что они не имеют одинаковое значение, даже если они имеют одно и то же имя. Согласно этой строгой интерпретации, остается только параметри c полиморфизм.
Для " параметри c полиморфизм ": значение [] имеет тип 'a list, но также имеет тип int list, real list, bool list и т. Д. Я не знаю, скажете ли вы, что у него бесконечно много типов, но я полагаю, вы могли бы сказать это. Но даже если бы вы сказали это, никакое значение типа 'a something не имело бы конечного числа n> 1 типов. И то же самое не относится к ('a, 'b) something и т. Д.
Я не могу придумать других способов для значения иметь более одного типа в SML, чем эти два вида полиморфизм. Интересный дополнительный вопрос заключается в том, существуют ли значимые способы определения значений в любой системе типов, имеющей n типов, где n> 1, кроме этих двух способов.
Если вопрос был «для каждые целых чисел n ≥ 0 существует ли тип , который имеет ровно n значений ?» ответ будет "да", так как для n = 1 у вас есть datatype One = One, для n = 2 у вас есть datatype Two = One | Two и так далее. Для n = 0 вы можете создать абстрактный / непрозрачный тип без открытых конструкторов. В Haskell этот тип просто data Void без = ... части, но при отсутствии этого синтаксиса в SML вы можете сделать что-то вроде:
signature VOID = sig type t end
structure Void :> VOID = struct type t = unit end
fun whyNot (x : Void.t) = "I wonder how one might call this function."
Даже если Void.t определяется как unit, он также сделан непрозрачным, скрывая конструктор значения ():
- whyNot ();
! Toplevel input:
! whyNot ();
! ^^
! Type clash: expression of type
! unit
! cannot have type
! Void.t
Таким образом, эквивалентность между Void.t и unit не раскрывается , давая тип Void.t 0 значений.