嵌套类型级编程答案

【问题标题】：Nested Type-Level Programming嵌套类型级编程
【发布时间】：2016-12-25 07:17:40
【问题描述】：

我正在尝试使用 DataKinds 进行类型级编程，但是当我将其中一个结构嵌套在另一个结构中时遇到了困难。

{-# LANGUAGE DataKinds, TypeFamilies, GADTs, MultiParamTypeClasses, FlexibleInstances #-}

module Temp where

data Prop1 = D | E 

data Lower :: Prop1 -> * where
  SubThing1 :: Lower D
  SubThing2 :: Lower E

class ClassLower a where
  somefunc2 :: a -> String

instance ClassLower (Lower D) where
  somefunc2 a = "string3"

instance ClassLower (Lower E) where
  somefunc2 a = "string4"

data Prop2 = A | B | C

data Upper :: Prop2 -> * where
  Thing1 :: Upper A
  Thing2 :: Upper B
  Thing3 :: Lower a -> Upper C

class ClassUpper a where
  somefunc :: a -> String

instance ClassUpper (Upper A) where
  somefunc a = "string1"

instance ClassUpper (Upper B) where
  somefunc a = "string2"

instance ClassUpper (Upper C) where
  somefunc (Thing3 x) = somefunc2 x

只要我添加了 ClassUpper 的最后一个实例，就会出现错误。

Temp.hs:37:25: error:
    • Could not deduce (ClassLower (Lower a))
        arising from a use of ‘somefunc2’
      from the context: 'C ~ 'C
        bound by a pattern with constructor:
                   Thing3 :: forall (a :: Prop1). Lower a -> Upper 'C,
                 in an equation for ‘somefunc’
        at /Users/jdouglas/jeff/emulator/src/Temp.hs:37:13-20
    • In the expression: somefunc2 x
      In an equation for ‘somefunc’: somefunc (Thing3 x) = somefunc2 x
      In the instance declaration for ‘ClassUpper (Upper 'C)’

我知道'C ~ 'C 表示类型相等，但我不明白根本问题是什么，更不用说解决方案或解决方法了。

我不明白什么，解决这个问题的最佳方法是什么？

【问题讨论】：

标签： haskell data-kinds

【解决方案1】：

这里的问题有点微妙。人们可能期望 GHC 接受这一点的原因是您拥有所有可能的 Lower a 的实例，因为您只提供了制作 Lower D 和 Lower E 的方法。但是，可以为Lower 构建一个病态定义，例如

import GHC.Exts (Any)

data Lower :: Prop1 -> * where
  SubThing1 :: Lower D
  SubThing2 :: Lower E
  SubThing3 :: Lower Any

重点是，不仅D 和E 有亲切的Prop1。我们可以玩这种恶作剧的不仅仅是Any之类的东西——甚至允许使用以下构造函数（所以F Int :: Prop1也是）！

  SubThing4 :: Lower (F Int)

type family F x :: Prop1 where {}

因此，总而言之，根本问题是 GHC 确实无法确定 ClassLower (Lower a) 约束（由于使用 somefunc2 而需要）是否会得到满足。为此，它必须做大量工作来检查 GADT 构造函数，并确保某个实例涵盖了所有可能的情况。

在这种情况下，您可以通过将ClassLower (Lower a) 约束添加到GADT 构造函数（启用FlexibleContexts）来解决您的问题。

data Upper :: Prop2 -> * where
  Thing1 :: Upper A
  Thing2 :: Upper B
  Thing3 :: ClassLower (Lower a) => Lower a -> Upper C

【讨论】：

【解决方案2】：

或者您可以像这样写出您的 ClassLower 实例，使用模式匹配（而不是类型变量）来区分 GADT 的情况：

instance ClassLower (Lower a) where
    somefunc2 SubThing1 = "string3"
    somefunc2 SubThing2 = "string4"

【讨论】：

对，那么你也可以把所有的类型类都去掉。