Haskell 无法从 GADT 构造函数中找出类型答案

【问题标题】：Haskell can't figure out types from GADT constructorHaskell 无法从 GADT 构造函数中找出类型
【发布时间】：2015-11-25 12:02:57
【问题描述】：

提前为长示例道歉，我想不出更短的示例。

让我们定义一个类型类Box，它只包含另一个类型Content。

{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE TypeFamilies              #-}

class Box t where
    type Content t

data IntBox = IntBox
data StringBox = StringBox

让我们写几个例子：

instance Box IntBox where
    type Content IntBox = Int

instance Box StringBox where
    type Content StringBox = String

data JointBox a b = JointBox a b

instance (Box a, Box b) => Box (JointBox a b) where
    type Content (JointBox a b) = Either (Content a) (Content b)

到目前为止，所有的编译和工作。输入 GADT。我想要一个由盒子及其内容构成的代数数据类型。构造函数完全决定盒子的类型。

data ABox t where
    AnIntBox :: IntBox -> ABox IntBox
    AStringBox :: StringBox -> ABox StringBox
    AnIntOrStringBox :: JointBox IntBox StringBox -> ABox (JointBox IntBox StringBox)

现在，在我看来，这意味着通过ABox 的构造函数上的模式匹配，应该确定框的类型及其内容。但这似乎并非如此：

frobABox :: (Content t) ->  ABox t              -> IO ()
frobABox     int           (AnIntBox _)         =  print $ int + 3
frobABox     string        (AStringBox _)       =  putStrLn $ reverse string
frobABox    (Left int)     (AnIntOrStringBox _) =  print $ int + 6
frobABox    (Right string) (AnIntOrStringBox _) =  putStrLn $ reverse string

这会引发很多错误，其中这两个对我来说似乎最重要：

GADTAndTypeClassBug.hs:29:14:
    Couldn't match expected type ‘Content t’
                with actual type ‘Either t0 t1’
    The type variables ‘t0’, ‘t1’ are ambiguous
    Relevant bindings include
      frobABox :: Content t -> ABox t -> IO ()
        (bound at GADTAndTypeClassBug.hs:27:1)
    In the pattern: Left int
    In an equation for ‘frobABox’:
        frobABox (Left int) (AnIntOrStringBox _) = print $ int + 6

GADTAndTypeClassBug.hs:30:14:
    Couldn't match expected type ‘Content t’
                with actual type ‘Either t2 t3’
    The type variables ‘t2’, ‘t3’ are ambiguous
    Relevant bindings include
      frobABox :: Content t -> ABox t -> IO ()
        (bound at GADTAndTypeClassBug.hs:27:1)
    In the pattern: Right string
    In an equation for ‘frobABox’:
        frobABox (Right string) (AnIntOrStringBox _)
          = putStrLn $ reverse string

GADTAndTypeClassBug.hs:30:71:
    Couldn't match expected type ‘[Char]’ with actual type ‘t3’
      ‘t3’ is untouchable
        inside the constraints (t ~ JointBox IntBox StringBox)
        bound by a pattern with constructor
                   AnIntOrStringBox :: JointBox IntBox StringBox
                                       -> ABox (JointBox IntBox StringBox),
                 in an equation for ‘frobABox’
        at GADTAndTypeClassBug.hs:30:29-46
    Relevant bindings include
      string :: t3 (bound at GADTAndTypeClassBug.hs:30:20)
    In the first argument of ‘reverse’, namely ‘string’
    In the second argument of ‘($)’, namely ‘reverse string’

一个没有类型族的更简单的例子：

data UnitOrEither t where
    AUnit :: () -> UnitOrEither ()
    AnEither :: Either String Int -> UnitOrEither (Either String Int)

frob :: UnitOrEither t -> IO ()
frob   (AUnit _)       =  print ()
frob   (AnEither _)    =  print "Either"

那么问题出在哪里？

【问题讨论】：

你不需要一个类型类来获得一个类型族。你可以写type family Content t; type instance (JointBox a b) = Either (Content a) (Content b)（IntBox/StringBox 也一样）。这是更少的代码，并且不会引入您不关心的类型级名称。
@DanielWagner，对，我只是简化了我正在使用的实际示例。

标签： haskell gadt type-families

【解决方案1】：

GADT 模式匹配的优化从左到右进行。因此，通过匹配 frobABox 的第二个参数而产生的类型细化将不适用于第一个。

你可以通过翻转frobABox的参数来编译代码：

frobABox' :: ABox t              -> Content t -> IO ()
frobABox' (AnIntBox _)          int           =  print $ int + 3
frobABox' (AStringBox _)        string        =  putStrLn $ reverse string
frobABox' (AnIntOrStringBox _) (Left int)     =  print $ int + 6
frobABox' (AnIntOrStringBox _) (Right string) =  putStrLn $ reverse string

frobABox :: (Content t) ->  ABox t              -> IO ()
frobABox = flip frobABox'

【讨论】：