Правильно ли я думаю и использую синглтон-типы в Haskell?

Question

Я хочу создать несколько несовместимых, но в остальном равных типов данных.То есть я хотел бы иметь параметризованный тип Foo a и такие функции, как

bar :: (Foo a) -> (Foo a) -> (Foo a) 

, на самом деле не заботясь о о том, что такое a.Чтобы уточнить далее, я бы хотел, чтобы система типов не давала мне делать

x :: Foo Int
y :: Foo Char
bar x y

, в то время как меня в то же время не волнуют Int и Char (меня интересует только то, что онине то же самое).

В моем реальном коде у меня есть тип для полиномов над данным кольцом.На самом деле меня не волнует, что такое неопределенность, пока система типов мешает мне добавить многочлен от t с многочленом от s.До сих пор я решил эту проблему путем создания класса типов Indeterminate и параметризации моего полиномиального типа как

data (Ring a, Indeterminate b) => Polynomial a b

Этот подход кажется совершенно естественным для части Ring, потому что я делаю заботиться о том, какое конкретное кольцо заданный полином закончен.Он выглядит очень надуманным для части Indeterminate, как подробно описано ниже.

Вышеупомянутый подход работает отлично, но выглядит надуманным.Особенно эта часть:

class Indeterminate a where
    indeterminate :: a

data T = T

instance Indeterminate T where
    indeterminate = T

data S = S

instance Indeterminate S where
    indeterminate = S

(и так далее, возможно, для еще нескольких неопределенностей).Это странно и неправильно.По сути, я пытаюсь потребовать, чтобы экземпляры Indeterminate были синглетонами (в в этом смысле ).Чувство странности - один из признаков того, что я могу атаковать это неправильно.Другим фактом является то, что мне приходится аннотировать много моих Polynomial a b с, поскольку фактический тип b часто не может быть выведен (это не странно, но, тем не менее, раздражает).

Есть предложения?Должен ли я просто продолжать делать это так, или я что-то упустил?

PS: Не обижайтесь, если я не возражаю или не принимаю ответы немедленно.Я не смогу вернуться в течение нескольких дней.

Answer 1

Прежде всего, я не уверен в этом:

data (Ring a, Indeterminate b) => Polynomial a b

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

Во-вторых, вас действительно интересует параметр «неопределенный», кроме того, чтобы гарантировать, что типы хранятся отдельно?Довольно стандартный способ сделать это - то, что называется фантомные типы - по сути, параметры в конструкторе типов, которые не используются в конструкторе данных.Вы никогда не будете использовать или нуждаться в значении фантомного типа, поэтому функции могут быть настолько полиморфными, как вы хотите, например:

data Foo a b = Foo b

foo :: Foo a b -> Foo a b
foo (Foo x) = Foo x

bar :: Foo a c -> Foo b c
bar (Foo x) = Foo x

baz :: Foo Int Int -> Foo Char Int -> Foo () Int
baz (Foo x) (Foo y) = Foo $ x + y

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

Мне кажется, что вышеупомянутый подход должен быть достаточным для того, что вы здесь делаете - бизнес с одноэлементными типами в основном сводится к преодолению разрыва междуболее сложные вещи на уровне типов и регулярные вычисления на уровне значений путем создания прокси типов для значений.Это может быть полезно, скажем, для маркировки векторов типами, которые указывают их основу, или для обозначения числовых значений физическими единицами - в обоих случаях аннотация имеет большее значение, чем просто «неопределенный элемент с именем X».