Типы Singleton в Haskell

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

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

Мой вопрос: как типы одноэлементных отличаются от типов классов или от цитируемых /reified структур в этом отношении?

Я также особо хотел бы получить некоторое интуитивное объяснение в отношении теоретико-теоретического значения/преимуществ использования одноэлементных типов и степени, в которой они могут эмулировать зависимые типы в целом.

Ответ 1

Как вы описали, singleton-типы - это те, которые имеют только одно значение (пусть игнорирует ⊥ на данный момент). Таким образом, значение одноэлементного типа имеет уникальный тип, представляющий значение. Суть теории зависимого типа (DTT) заключается в том, что типы могут зависеть от значений (или, иначе говоря, значения могут параметризовать типы). Теория типов, которая позволяет типам зависеть от типов, может использовать одноэлементные типы, чтобы типы зависели от значений одиночного элемента. Напротив, классы типов предоставляют специальный полиморфизм, где значения могут зависеть от типов (наоборот, для DTT, где типы зависят от значений).

Полезным методом в Haskell является определение класса связанных одноэлементных типов. Классический пример - натуральные числа:

data S n = Succ n 
data Z = Zero

class Nat n 
instance Nat Z
instance Nat n => Nat (S n)

Если дополнительные экземпляры не добавлены в Nat, класс Nat описывает одноэлементные типы, значения/типы которых являются индуктивно определенными натуральными числами. Заметим, что Zero является единственным жителем Z, но тип S Int, например, имеет много обитателей (он не одиночный); класс Nat ограничивает параметр S для одноэлементных типов. Интуитивно, любой тип данных с несколькими конструкторами данных не является одиночным типом.

Дайте вышеизложенное, мы можем написать зависимую функцию-преемника:

succ :: Nat n => n -> (S n)
succ n = Succ n

В сигнатуре типа переменная типа n может рассматриваться как значение, поскольку ограничение Nat n ограничивает n классом одноэлементных типов, представляющих натуральные числа. Тип возврата succ затем зависит от этого значения, где S параметризуется значением n.

Любое значение, которое может быть индуктивно определено, может быть дано уникальным представлением одноэлементного типа.

Полезным методом является использование GADT для параметризации не одиночных типов с одноточечными типами (то есть со значениями). Это можно использовать, например, для представления типа на уровне формы индуктивно определенного типа данных. Классическим примером является размерный список:

data List n a where
   Nil :: List Z a 
   Cons :: Nat n => a -> List n a -> List (S n) a

Здесь одиночные типы натурального числа параметризуют тип списка по его длине.

Мышление в терминах полиморфного лямбда-исчисления, succ выше принимает два аргумента, тип n, а затем параметр значения типа n. Таким образом, типы singleton здесь представляют собой Π-тип, где succ :: Πn:Nat . n -> S(n), где аргумент succ в Haskell предоставляет как зависимый параметр продукта n:Nat ( передается как параметр типа), а затем значение аргумента.