Как определить функцию внутри haskell newtype?

Question

Я пытаюсь расшифровать синтаксис записи в haskell для newtype, и мое понимание ломается, когда есть функция внутри newtype. Рассмотрим этот простой пример

newtype C a b = C { getC :: (a -> b) -> a } 

согласно моему мотивировочной C это тип, который принимает функцию и параметр в его конструктор. так,

let d1 = C $ (2 *) 3 

:t d1 также дает

d1 :: Num ((a -> b) -> a) => C a b 

Снова проверить это я :t getC d1, который показывает этот

getC d1 :: Num ((a -> b) -> a) => (a -> b) -> a 

Почему ошибка при попытке getC d1? getC должен возвращать функцию и ее параметр или, по крайней мере, применять параметр.

У меня не может быть newtype C a b = C { getC :: (a->b)->b } deriving (Show), потому что это не имеет смысла!

Answer 1

По моему мотивировочной C это тип, который принимает функцию и параметр

Как так? Конструктор имеет только один аргумент. Newtypes всегда имеют один конструктор с одним аргументом.

Тип C, otoh, имеет два типа параметров. Но это не имеет никакого отношения к числу аргументов, которые вы можете применить к конструктору.

Answer 2

Это всегда хорошо, чтобы подчеркнуть, что Haskell имеет два совершенно разных пространств имен, в типа языка и язык значение. В вашем случае есть

• Тип конструктора C :: * -> * -> *, который живет на языке типа. Требуется два типа: a, b (вида *) и сопоставляет их с типом C a b (также вида *).
• Конструктор значений C :: ((a->b) -> a) -> C a b, который живет на языке значений. Требуется функция f (типа (a->b) -> a) и сопоставляет ее со значением C f (типа C a b).

Возможно, было бы менее запутанным, если у вас

newtype CT a b = CV ((a->b) -> a) 

а потому, что для Newtype всегда точно один конструктор значение (а именно один конструктор типа), имеет смысл называть их так же.

CV - конструктор значений, который принимает одну функцию, полную остановку. Эта функция будет иметь подпись (a->b) -> a, т. Е. Ее аргумент также является функцией, но в отношении CT это не имеет большого значения.

Действительно, это отчасти неправильно, что data и newtype декларации использовать = символ, потому что это не означает, что вещи на правой и левой “ то же ” – не может, потому что они даже не принадлежат на тот же язык. Там это альтернативный синтаксис, который выражает отношение лучше:

{-# LANGUAGE GADTs #-} 

data CT :: * -> * -> * where 
    CV :: ((a->b) -> a) -> CT a b 

Что касается этого значения вы пытались построить

let d1 = CV $ (\x->(2*x)) 3

здесь вы сделали не пас “ функцию и параметр ” - CV. Что вы на самом деле сделали был, вы применили функцию \x->2*x к значению 3 (возможно, также написали 6) и передали этот номер CV. Но, как я уже сказал, CV ожидает функцию. Что тогда происходит, GHC пытается интерпретировать 6 как функцию, которая дает фиктивное ограничение Num ((a->b) -> a). Что это означает: “, если (a->b)->a - это номер, то ... ”. Конечно это не a номер type, so the rest doesn't make sense either.

---

_{Это потому, что $ имеет самый низкий приоритет, то есть выражение CV $ (\x->(2*x)) 3 фактически анализируется как CV ((\x->(2*x)) 3), или, что эквивалентно let y = 2*3 in CV y.}