haskell - 如何在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

强调 Haskell 有两个完全独立的 namespace 总是好的，类型语言 和值语言。在你的情况下，有

• 类型构造函数 C::Type -> Type -> Type，它存在于类型语言中。它需要两种类型 a、b(属于 Type)并将它们映射到类型 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 #-}

import Data.Kind

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

至于你试图构建的值(value)

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

这里您没有将“一个函数和一个参数”传递给CV。您实际做的^‡ 是，您将函数\x->2*x 应用于值3(也可以写成6) 并将该数字传递给 CV。但正如我所说，CV 需要一个函数。然后发生的是，GHC 试图将 6 解释为一个函数，它给出了伪造的约束 Num ((a->b) -> a)。这意味着:“如果 (a->b)->a 是数字类型，那么......”。当然，它不是数字类型，so the rest doesn't make sense either .

---

^†_{谈论“types of kind Type”似乎有些多余。实际上，在谈论“类型”时，我们通常指的是“类型级语言中的实体”。这些有种类(“类型级类型”)，其中 Type(^(lifted) 值的种类-level 值)是最突出的，但不是唯一的——你也可以有类型级的数字和类型级的函数——C 确实是一个。
请注意 类型 历史上写成 *，但这种表示法已被弃用，因为它不一致(与乘法运算符混淆)。}

^‡_{这是因为 $ 的优先级最低，即表达式 CV $ (\x->(2*x)) 3 实际上被解析为 CV ((\x->(2*x)) 3)，或者等效地 let y = 2*3 in CV y。}