Сомнения в поведении Unit Type в системе типов

Question

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

Начнем с того, что Тип устройства может рассматриваться как нулевой тип продукта, а именно Unit, с одним единственным значением, которое является пустым кортежем, ().Кроме того, существует уникальный сопоставьте с любым типом объекта.

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

datatype suit = HEARTS | CLUBS | DIAMONDS | SPADES

где ЧЕРВИ, ТРЕФЫ, БУБНЫ и ПИКИ являются нулевыми типами продуктов и, следовательно, все они изоморфны единице измерения.

Мое сомнение заключается в следующем:если существует только один элемент Unit, как система типов может различать четыре различных экземпляра, используемых в приведенном выше типе Sum (пять экземпляров, если мы также рассмотрим пустой кортеж...)?Я понимаю, что все они могут считаться равными друг другу с точностью до изоморфизма, но они различны в расширении и на самом деле, даже рассматривая только suit предполагается, что мы должны сопоставлять их с образцом...

Answer 1

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

Обратите внимание, что аспект сопоставления с образцом является ортогональным:вы можете думать о пяти типах единиц измерения как о существующих изолированно.В большинстве теорий типов вы можете взять сумму любых двух типов, даже двух, которые (номинально) равны, например Unit + Unit.От вас по-прежнему потребуется соответствие шаблону, и у вас будет два случая:левый Unit и правильный Unit.Номинальный аспект неважен, хотя многие языки программирования будут использовать имена для различения различных случаев, подобных этому, вместо индексов слагаемых (в частности, в языках, где вам разрешено принимать суммы только различных номинальных типов, таких как стандартный ML).