嵌套类型级编程

Question

我正在尝试使用 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 表示类型相等，但我不明白潜在的问题是什么，更不用说解决方案或解决方法了。

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

Answer 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

Answer 2

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

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

嵌套类型级编程

Nested Type-Level Programming

haskell

data-kinds