Типы Singleton в Haskell

Question

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

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

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

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

Answer 1

Как вы описали, одноэлементные типы - это те, которые имеют только одно значение (давайте не будем отмечать ⊥). Таким образом, значение одноэлементного типа имеет уникальный тип, представляющий значение. Суть теории зависимого типа (DTT) заключается в том, что типы могут зависеть от значений (или, иначе говоря, значения могут параметризовать типы). Теория типов, которая позволяет типам зависеть от типов, может использовать одноэлементные типы, чтобы типы зависели от значений одиночного элемента. Напротив, классы типов предоставляют ad hoc полиморфизм, где значения могут зависеть от типов (наоборот, для 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. Таким образом, одноэлементные типы здесь представляют собой вид Π-type, где succ :: Πn:Nat . n -> S(n), где аргумент succ в Haskell предоставляет как зависимый параметр продукта n:Nat (передан как параметр типа), так и значение аргумента.