Haskell, используя классы типов внутри сигнатуры типа

Question

Предполагая простой класс типов ограниченной подпись:

f :: (Eq a, Num b) => a -> b 
f str = 4 

Я задавался вопрос, почему они не работают

f :: (Eq a) -> (Num b) 
f str = 4 

f :: Eq -> Num 
f str = 4 

Я знаю, что классы типа имеют вид * -> Constraint, в то время как подписи типа допускают только виды *.

Но мой вопрос, почему это ограничение? Почему нельзя использовать типы типов как типы? Каковы были бы преимущества и недостатки, позволяющие использовать стили типа типа?

Answer 1

Существует (если мы пренебрегаем unboxed types) только один вид, типы которого действительно имеют любые значения: *. Все остальные типы не содержат типов как таковых, а просто «сущности типа». Компилятор может использовать их для определения , что делать с фактическими типами и их значениями вокруг, но никогда не возможно иметь во время выполнения значение типа с каким-то вроде * -> Constraint.

Это * вид для типов значений - это просто правило игры. Хорошо, что по той же причине неплохо иметь сильную систему статического типа, которая предотвращает бессмысленные преобразования во время выполнения. ^Wat?? Или, давайте возьмем это буквально, по той же причине вы не можете просто прыгнуть своего короля над своими пешками, независимо от того, насколько привлекательна эта особенность в конкретной ситуации, в которой вы столкнулись.

Если какое-либо расширение позволило сделать значения из не-* -имя типов, в частности * -> Constraint, нам понадобится целая куча неочевидных определений, чтобы дать понять, как эти «значения класса» на самом деле должны использоваться. Вероятно, это будет означать тип записи, содержащий методы класса в качестве словаря. Но, как точно ... спецификация будет в значительной степени кошмаром. И усложнение языка таким образом никоим образом не стоит затрат, так как 1. стандартный способ использования классов типов просто хорош для не менее 95% всех приложений и 2., когда вам нужен тип reified классы, вы можете легко сделать это с помощью GADT, ConstraintKinds или даже с обычными старыми вручную записями словаря. Ничто из этого не требует искажения основополагающих идей о том, как язык относится к значениям, как к типам *.

---

... Во всяком случае давайте рассмотрим на минуту, как это мощь работы. Одно можно сказать наверняка: это не позволит вам писать что-нибудь простое, как f str = 4!

Рассмотрим

f1 :: forall a, b . Eq a -> Num b 

Eq a, Num b :: Constraint И, таким образом, мы должны были бы значения типа любезного Constraint. Это будет в основном конкретным словарем методов для данного экземпляра. Таким образом, реализация f1 придется искать что-то вроде

f1 (EqDict (d_eq :: a -> a -> Bool)) 
     = NumDict { dict_fromInteger = ??? :: Integer -> b 
       , dict_plus  = ??? :: b -> b -> b 
       , ... 
       , dict_signum  = ??? :: b -> b 
       } 

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

monadApp :: forall m . Monad m -> Applicative m 
monadApp (MonadDict {dict_return = d_ret, dict_bind = d_bd}) 
     = ApplicativeDict { dict_pure = d_ret 
          , dict_app = \fs vs -> d_bd fs (\f -> d_bd vs $ d_ret . f) } 

Это конкретный один будет, на самом деле, несколько полезно, но только потому, что Monad (still, but not for long!) не хватает Applicative как суперкласс, который он должен просто иметь. Как правило, не должно быть много причин, чтобы явно «понизить» любые классы, потому что суперкласс-отношения (или кортежи-ConstraintKinds) делают это автоматически.

Answer 2

Тип переменные могут появляться более чем один раз в сигнатуре типа:

f :: Eq a => a -> a -> a -> Bool 

Дать выше, как

f :: Eq a -> Eq a -> Eq a -> Bool 

выглядит неудобно. Хуже того, мы могли бы иметь более одного ограничения на a:

g :: (Show a, Eq a) => a -> Bool 

Как бы мы записали это в альтернативной нотации?

g :: (Show & Eq) a -> Bool -- ?? 

Забыв a полностью, как вы предлагаете, в последнем примере делает подпись неоднозначными: рассмотреть

h1 :: (Eq a)  => a -> a -> a -> a -> Bool 
h2 :: (Eq a, Eq b) => a -> a -> b -> b -> Bool 

Это совершенно разные подписи: вы можете позвонить h2 1 2 [1] [2], но не h1 1 2 [1] [2] , поскольку последний требует четыре аргумента одного типа. После используются в предлагаемой конвенции, они сводятся к одной и той же подписи:

h12 :: Eq -> Eq -> Eq -> Eq -> Bool 

ли вызов h12 1 2 [1] [2] действительных? Вышеприведенная подпись слишком неоднозначна.