考虑这个代码:
{-# LANGUAGE GADTs #-}
data P t where
PA :: P Int
PB :: P Double
PC :: P Char
isA PA = True
isA _ = False
它编译并运行良好。现在考虑这个代码:
{-# LANGUAGE GADTs #-}
data P t where
PA :: P Int
PB :: P Double
PC :: P Char
isA PA = True
isA PB = False
isA PC = False
它无法编译:
Main.hs:8:10: error:
• Couldn't match expected type ‘p’ with actual type ‘Bool’
‘p’ is untouchable
inside the constraints: t ~ Int
bound by a pattern with constructor: PA :: P Int,
in an equation for ‘isA’
at Main.hs:8:5-6
‘p’ is a rigid type variable bound by
the inferred type of isA :: P t -> p
at Main.hs:(8,1)-(10,14)
Possible fix: add a type signature for ‘isA’
• In the expression: True
In an equation for ‘isA’: isA PA = True
• Relevant bindings include isA :: P t -> p (bound at Main.hs:8:1)
|
8 | isA PA = True
| ^^^^
Main.hs:9:10: error:
• Couldn't match expected type ‘p’ with actual type ‘Bool’
‘p’ is untouchable
inside the constraints: t ~ Double
bound by a pattern with constructor: PB :: P Double,
in an equation for ‘isA’
at Main.hs:9:5-6
‘p’ is a rigid type variable bound by
the inferred type of isA :: P t -> p
at Main.hs:(8,1)-(10,14)
Possible fix: add a type signature for ‘isA’
• In the expression: False
In an equation for ‘isA’: isA PB = False
• Relevant bindings include isA :: P t -> p (bound at Main.hs:8:1)
|
9 | isA PB = False
| ^^^^^
Main.hs:10:10: error:
• Couldn't match expected type ‘p’ with actual type ‘Bool’
‘p’ is untouchable
inside the constraints: t ~ Char
bound by a pattern with constructor: PC :: P Char,
in an equation for ‘isA’
at Main.hs:10:5-6
‘p’ is a rigid type variable bound by
the inferred type of isA :: P t -> p
at Main.hs:(8,1)-(10,14)
Possible fix: add a type signature for ‘isA’
• In the expression: False
In an equation for ‘isA’: isA PC = False
• Relevant bindings include isA :: P t -> p (bound at Main.hs:8:1)
|
10 | isA PC = False
| ^^^^^
为什么?这里发生了什么?
编辑:添加类型签名
isA :: P t -> Bool
使它起作用,所以我现在的问题变成:为什么类型推断在第二种情况下不起作用,因为它在第一种情况下起作用?
最佳答案
在 中键入 case 构造(无论是显式 case
语句还是隐式基于模式的函数定义)缺席 GADTs,个别的替代品:
pattern -> body
可以通过键入所有模式并将其与被检查者的类型统一,然后键入所有主体并将其与
case
的类型统一。整体表达。所以,在一个简单的例子中,如:data U = UA | UB | UC
isA1 u = case u of
UA -> True
UB -> False
x -> False
我们可以首先输入模式
UA :: U
, UB :: U
, x :: a
, 使用类型相等 a ~ U
统一它们推断被审查者的类型 u :: U
,同样统一 True :: Bool
和 False :: Bool
到整体 case 表达式的类型 Bool
,将其与 isA
的类型统一起来获取 isA :: U -> Bool
.请注意,统一过程可以使类型特化。在这里,模式的类型
x :: a
是通用的,但在统一过程结束时,它已专门用于 x :: U
.这也可能发生在 body 上。例如:len mstr = case mstr of
Nothing -> 0
Just str -> length str
在这里,
0 :: Num a => a
是多态的,但因为 length
返回 Int
,到过程结束时,主体(以及整个 case 表达式)已统一为类型 Int
.一般来说,通过统一,所有主体的公共(public)、统一类型(以及整个 case 表达式的类型)将是“最一般”/“限制最少”的类型,其中主体的类型都是泛化。在某些情况下,这种类型可能是其中一个实体的类型,但一般来说,所有实体都可以比“最一般”的统一类型更通用,但没有任何实体可以更具限制性。
在 GADT 的存在下,情况会发生变化。当使用 GADT 进行类型检查 case 构造时,替代方案中的模式可以引入“类型细化”,即一组附加的类型变量绑定(bind),用于对替代方案的主体进行类型检查。 (这就是首先使 GADT 有用的原因。)
因为不同替代品的 body 是在不同的细化下键入的,所以不可能进行天真的统一。例如,考虑微型类型的 DSL 及其解释器:
data Term a where
Lit :: Int -> Term Int
IsZ :: Term Int -> Term Bool
If :: Term Bool -> Term a -> Term a -> Term a
eval :: Term a -> a
eval t = case t of
Lit n -> n
IsZ t -> eval t == 0
If b t e -> if eval b then eval t else eval e
如果我们天真地统一 body
n :: Int
, eval t == 0 :: Bool
, 和 if eval b then eval t else eval e :: a
,程序不会进行类型检查(最明显的是,因为 Int
和 Bool
不统一!)。一般来说,因为类型改进允许替代体的计算类型比最终类型更具体,所以没有明显的“最通用”/“限制最少”的类型可以统一所有体,就像没有 GADT 的 case 表达式。
相反,我们通常需要为整个 case 表达式提供一个“目标”类型(例如,对于
eval
,类型签名中的返回类型 a
),然后确定是否在每个由构造函数引入的细化下(例如,IsZ
引入细化 a ~ Bool
),主体 eval t == 0 :: Bool
具有相关的细化 a
作为其类型.如果没有明确提供目标类型,那么我们能做的最好的事情——一般来说——是使用一个新的类型变量
p
作为目标并尝试检查每个改进的类型。这意味着,给定以下定义,没有
isA2
的类型签名:data P t where
PA :: P Int
PB :: P Double
PC :: P Char
isA2 = \p -> case p of
PA -> True
PB -> False
PC -> False
GHC 试图做的是输入
isA2 :: P t -> p
.对于替代方案:PA -> True
它类型
PA :: P t
给予细化 t ~ Int
,在这种改进下,它尝试输入 True :: p
.不幸的是,p
不是 Bool
在涉及无关类型变量 a
的任何细化下,我们得到一个错误。其他替代方案也会产生类似的错误。实际上,我们还可以做一件事。如果有没有引入类型细化的替代方案,那么它们的主体的计算类型是 不是 比最终类型更具体。因此,如果我们统一“未精炼”备选方案的主体类型,则结果类型为经过提炼的备选方案提供了合法的统一目标。
这意味着,例如:
isA3 = \p -> case p of
PA -> True
x -> False
第二种选择:
x -> False
通过匹配模式
x :: P t
输入这不引入类型细化。粗体型为Bool
,并且这种类型是统一其他替代方案的合适目标。具体来说,第一种选择:
PA -> True
与类型细化匹配
a ~ Int
.在这种细化下, body 的实际类型True :: Bool
匹配目标类型的“细化”Bool
(“精炼”为 Bool
),并且确定替代品具有有效类型。因此,直觉是,如果没有通配符替代,case 表达式的推断类型是任意类型变量
p
,这太笼统了,无法与类型提炼替代方案统一。但是,当您添加通配符大小写替代时 _ -> False
,它引入了更严格的体型 Bool
进入统一过程,由模式 _
推导出没有任何类型细化, 可以通过提供更严格的类型 Bool
来通知统一算法可以统一其他类型的精制替代品。上面,我认为有一些两阶段方法,其中首先检查“非精炼”替代方案以确定目标类型,然后对照它检查精炼替代方案。
事实上,细化过程将新变量引入到统一过程中,即使它们被统一,也不会影响更大的类型上下文。因此,所有备选方案同时统一,但未精炼备选方案的统一会影响较大类型的上下文,而精炼备选方案的统一会影响一堆新变量,得出的最终结果与未精炼和完善的备选方案分别处理一样。
关于haskell - 为什么在枚举所有情况时通配符匹配不起作用?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/60994280/