haskell - 具有类似 gadt 约束的新类型

Question

我明白为什么你不能这样做：

{-# LANGUAGE GADTs  #-}

newtype NG a  where MkNG :: Eq a => a -> NG a

-- 'A newtype constructor cannot have a context in its type', says GHC

那是因为“数据”构造函数MkNG并不是真正的构造函数。“表达式中的构造函数N将值从类型t强制转换为类型……”语言报告第 4.2.3 节说“与代数数据类型不同，newtype 构造函数N是未提升的，……”

如果它能够支持一个约束，它需要一个约束字典的参数位置。

现在我已经引起了你的注意，我要问的是那个不推荐使用的功能，你经常看到（非常老的）StackOverflow 回答说要改用 GADT：

{-# LANGUAGE DatatypeContexts  #-}             -- deprecated ~2010

newtype Eq a => NC a = MkNC a                  -- inferred MkNC :: Eq a => a -> NC a

-- nc = MkNC (id :: Int -> Int)                -- rejected no Eq instance

quux (MkNC _) = ()                             -- inferred quux :: Eq a => NC a -> ()
quuz (x :: NC a) = ()                          -- inferred quuz :: NC a -> ()

（该类型quuz是 DatatypeContexts 的烦恼之一：因为构造函数没有出现在模式匹配中，所以类型推断无法“看到”约束。）

因此，这在数据类型上与 DatatypeContexts 一样好（或不好）（或不取决于您的观点）。

我的问题是：如何？MkNC 再次只是强制一个值/未解除。它是否使用字典传递来应用约束？鉴于强制纯粹是编译时效应，字典在哪里插入？

标签： haskelltypeclassgadtnewtype