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

Я пытаюсь расшифровать синтаксис записи в 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)потому что это не имеет смысла!

2 ответа

Согласно моим рассуждениям, C - это тип, который принимает функцию и параметр.

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

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

Всегда приятно подчеркнуть, что в 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)

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

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, То, что вы на самом деле сделали 1, вы применили функцию \x->2*x к стоимости 3 (с таким же успехом мог бы написать 6) и передал этот номер CV, Но, как я уже сказал, CV ожидает функцию. Затем происходит то, что GHC пытается интерпретировать 6 как функция, которая дает фиктивное ограничение Num ((a->b) -> a), Что это значит: "если (a->b)->a тип числа, то... ". Конечно, это не числовой тип, поэтому и остальное не имеет смысла.


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

Другие вопросы по тегам