GHC接受此代码，但它应该是非法的语法（？）关于正在发生什么的任何猜测？
module Tilde where
~ x = x + 2 -- huh?
~ x +++ y = y * 3 -- this makes sense
该(+++)方程式很有意义：它使用infix语法声明一个运算符，并在第一个参数上使用不可辩驳的模式匹配。
第一个“方程式”看起来与开始时一样。但是没有运算符。如果我问
?> :i ~
===> <interactive>:1:1: error: parse error on input `~'
?> :i (~)
===> class (a ~ b) => (~) (a :: k) (b :: k)
-- Defined in `Data.Type.Equality'
instance [incoherent] forall k (a :: k) (b :: k). (a ~ b) => a ~ b
-- Defined in `Data.Type.Equality' …这三者之间的差异是什么/为什么？GADT(和常规数据类型)只是数据系列的简写吗？具体来说有什么区别:
data GADT a where
MkGADT :: Int -> GADT Int
data family FGADT a
data instance FGADT a where -- note not FGADT Int
MkFGADT :: Int -> FGADT Int
data family DF a
data instance DF Int where -- using GADT syntax, but not a GADT
MkDF :: Int -> DF Int
(这些例子是否过于简化,所以我没有看到差异的微妙之处？)
数据系列是可扩展的,但GADT则不可扩展.OTOH数据族实例不得重叠.所以我无法声明另一个实例/任何其他构造函数FGADT; 就像我不能声明任何其他构造函数GADT.我可以声明其他实例DF.
通过这些构造函数上的模式匹配,等式的rhs确实"知道"有效载荷是Int.
对于类实例(我很惊讶地发现)我可以编写重叠实例来使用GADT:
instance C (GADT a) ...
instance {-# OVERLAPPING #-} C (GADT Int) ... …在关于GADT的问题之后，我正在尝试构建一个EDSL（例如本文中的示例），但是没有GADT。我已经做了一些工作，可以避免将AST的数据类型加倍。但是相反，它似乎使代码加倍。所以我试着减少代码，这是我遇到麻烦的地方...
而不是像这样的GADT
data Term a where
Lit :: Int -> Term Int
Inc :: Term Int -> Term Int
IsZ :: Term Int -> Term Bool
-- etc
将每个构造函数声明为单独的数据类型
data Lit = Lit Int deriving (Show, Read)
data Inc a = Inc a deriving (Show, Read)
data IsZ a = IsZ a deriving (Show, Read)
-- etc
然后，EDSL用户可以输入和show条款
aTerm = IsZ (Inc (Lit 5))
illtypedTerm = Inc (IsZ (Lit 5)) -- accepted OK and can show …GADT的优点的典型示例代表DSL的语法; 说这里的维基或在PLDI 2005年纸.
我可以看到,如果你通过构造得到一个类型正确的AST,那么编写一个eval函数很容易.
如何将GADT处理构建到REPL中？或者更具体地说是Read-Parse-Typecheck-Eval-Print-Loop？我看到你只是将eval步骤的复杂性推到了前面的步骤中.
GHCi是否在内部使用GADT来表示它正在评估的表达式？(表达式比典型的DSL要厚很多.)
首先,您不能derive Show使用GADT,因此对于Print步骤,您可以手动滚动Show实例或类似的内容:
{-# LANGUAGE GADTs, StandaloneDeriving #-}
data Term a where
Lit :: Int -> Term Int
Inc :: Term Int -> Term Int
IsZ :: Term Int -> Term Bool
If :: Term Bool -> Term a -> Term a -> Term a
Pair :: (Show a, Show b) => Term a -> Term b -> Term (a,b)
Fst :: (Show …使用PatternSynonyms（显式双向形式），模式到表达式的方程实际上形成了一个函数，但拼写为大写（前提是您最终得到正确类型的完全饱和的数据构造）。然后考虑（在 GHC 8.10.2）
{-# LANGUAGE PatternSynonyms, ViewPatterns #-}
data Nat = Zero | Succ Nat deriving (Eq, Show, Read)
-- Pattern Synonyms as functions?
pattern Pred :: Nat -> Nat
pattern Pred n <- {- what goes here? -} where
Pred (Succ n) = n
pattern One = Succ Zero
zero = Pred One -- shows as Zero OK
那么我应该为pattern Pred n <- ???价值到模式的顶线设置什么？或者我不能Pred n在模式匹配中使用？似乎有效（但我不明白为什么）是一种视图模式
pattern Pred n <- (Succ -> n) …这个问题（从 5 年前开始）问“为什么所有递归模式同义词都被拒绝？” 它的例子仍然被拒绝。用户指南说“模式同义词不能递归定义”。
我有一个被接受的递归模式同义词（GHC 8.10.2）。我可以调用它，它会循环——这并不奇怪。那么为什么它会编译？/对于这样的事情是否有合理的用例？
代码基于2016 年论文的第 2.3 节“多态模式同义词”中的示例。
data JoinList a = JNil | Unit a | JoinList a `JoinTree` JoinList a deriving (Eq, Read, Show)
我正在尝试定义一个模式同义词Nil。显然JNil是一场比赛。而且JNil ``JoinTree`` JNil，任何JoinTree提供所有叶子的任意嵌套都是JNil.
pattern Nil :: JoinList a
pattern Nil <- JNil
where Nil = Nil `JoinTree` Nil -- huh?
wot = Nil `JoinTree` Nil -- these all compile
wotwot Nil = ()
wotwotwot = wotwot Nil
wotwotwotwot …如果我使用类型类重载方法，则以“字典传递样式”实现。也就是说，该方法有一个额外的参数（在表面Haskell中不会出现）。为了解决重载，该方法通过其“适当”参数的类型查找字典；并从字典中拉出方法实现。如此q中所述。
但是没有方法的类型类呢？它们可以用作约束。他们有字典吗？它包含什么？
对于一个特定的例子：
module M where
class C a -- no methods
-- no instances in module M
f :: C a => a -> Bool
f x = blah
C该模块中没有适用的实例，因此，如果M将其导入到其他模块（带有C实例）中，则如何f对字典查找进行编码？
通常的情况是该类C具有方法。有人呼吁他们方程的RHS f；因此通缉将C a被编码为方法调用的字典查找。
补充q ：（如果有人还在听）
2a。对于具有超类约束的无方法类型类：约束在字典中的位置在哪里？SPJ对票证的评论似乎表明这是字典数据构造函数的一个参数。
2b。对于带有约束的无方法类型类实例：约束再次在字典中的什么位置？
动机
@Daniel在评论中问这些q的动机。除了仅了解编译器内部知识外，还可以...
GHC将表面Haskell转换为内部表示形式：System F C，该系统在每个函数应用程序中都具有明显的类型签名。（这些应用程序必须包括对类的字典进行申请。）我试图了解类和实例decl的所有与类型相关的组件在字典中的位置。找出F C中的术语如何与原始Haskell等效。然后，我不理解[没有方法的类型类]如何适合。因为这些类不能直接作为表面Haskell中的术语出现，而只能作为约束出现。然后，对于此类在术语级别代表其的类，它必须是字典。
如果您想问这是怎么回事：F C中似乎存在一个局限性，即它不能表示功能依赖关系。与无法生成类型级别的证据有关。然后，我想了解这种限制是如何产生的/关于FunDeps不能（或目前没有）代表什么？
给定一个两位数据构造函数，我可以将其部分应用于一个参数，然后将其应用于第二个参数。为什么我不能使用相同的语法进行模式匹配？
data Point = MkPoint Float Float
x = 1.0 :: Float; y = 2.0 :: Float
thisPoint = ((MkPoint x) y) -- partially apply the constructor
(MkPoint x1 y1) = thisPoint -- pattern match OK
((MkPoint x2) y2) = thisPoint -- 'partially apply' the pattern, but rejected: parse error at y2
((MkPoint x3 y3)) = thisPoint -- this accepted, with double-parens
我为什么要这么做？我想获取构造函数和第一个参数作为 as 模式，这样我就可以将其应用于不同的第二个参数。（是的，这个例子中的解决方法很简单。实际上，我有一个更复杂的模式，有几个参数，我想将其中的最后一个参数分开。）：
(mkPx@(MkPoint x4) y4) = thisPoint -- also parse error
thatPoint = mkPx (y4 * 2)
comp5 :: [ Either Int Int ]
comp5 = [ Right x | {- Just y <- Just 2, -} let x = 5, y <- [x, undefined] ]
-- ^^ rejected: RHS must be list, `let` accepted
注释掉的内容Just y <- Just 2被拒绝类型错误，因为 RHS 不是列表 - 好的。
被let x = 5接受，即使它的左边没有发电机——预期的吗？
已y <- ...接受，但有警告Defined but not used:- 好的。
comp5的值是[Right 5,Right 5]——这是你所期望的吗？
...因为它是y <- ...从包含两个元素的列表生成的，即使y没有在任何地方使用。所以它充当“多重生成器”；即使它的左边没有发电机。
do …
有很多关于GADTs比 更好的问答DatatypeContexts，因为 GADT 会自动在正确的位置提供约束。例如这里，这里，这里。但有时似乎我仍然需要一个明确的约束。这是怎么回事？改编自此答案的示例：
{-# LANGUAGE GADTs #-}
import Data.Maybe -- fromJust
data GADTBag a where
MkGADTBag :: Eq a => { unGADTBag :: [a] } -> GADTBag a
baz (MkGADTBag x) (Just y) = x == y
baz2 x y = unGADTBag x == fromJust y
-- unGADTBag :: GADTBag a -> [a] -- inferred, no Eq a
-- baz :: GADTBag a -> Maybe [a] -> …使用InstanceSignatures，我可以为实例 decl 中的方法签名。
实例声明中的类型签名必须比类声明中的类型签名更多（或相同），使用实例类型实例化。
我可以从这个答案中看到sig 的类型部分不能更具体；但是为什么不能添加额外的约束呢？毕竟，您可以对实例 decl 施加约束，这将使实例比“使用实例类型实例化的类声明”更具体。
Addit：（响应前几条评论。）为了解释“您可以对实例 decl 进行约束……更具体的OVERLAPPABLE实例”：这里的实例头声称它提供addNat了所有类型a, b, c。但它没有：它只提供 if ais of the form SNat a'、cis of the formSNat c'等。我在问为什么我不能在方法级别同样限制类型？
例如[改编自 Hughes 1999]（更现实地说，这可能是 BST/玫瑰树等）：
data AscList a = AscList [a] -- ascending list
instance Functor AscList where -- constructor class
fmap f (AscList xs) = AscList $ sort $ fmap f xs
-- :: Ord …Prelude> let (Just x) = Just (x - 1) in x
*** Exception: <<loop>>
为什么编译器接受那个 decl？它可以在语法上告诉它绑定到循环（？）
GHC 知道：
Prelude> :set -XBangPatterns
Prelude> let !(Just x) = Just (x - 1) in x
Recursive bang-pattern or unboxed-tuple bindings aren't allowed:
[ ExceptionGHCi 7.10.2 上的那个和编译器失败消息。在 GHC 8.10 没有有用的消息，只是循环。]
递归模式绑定是否有一些合理的用途？我认为对于模式绑定 decl，lhs 的自由变量应该与 rhs(?)
我所说的“模式绑定”是指根据 Haskell 语言报告 2010 的第 4.4.3.2 节，特别是从数据构造函数/最外层范围开始的 lhs。
（我希望有比 lhs 上的单个 var 更令人兴奋的东西。这仍然算作“模式绑定”，请参阅评论。）
当然对于函数decls，编译器必须允许递归，因为它无法从语法上判断函数是否会循环：
Prelude> let { f 0 = 0;
f x = f (x - 1) } …