封闭类型家族内的模式匹配

Question

我无能地尝试使用 GHC 7.8 的新封闭类型系列功能，我想找到一种在类型级别构造上进行分支的好方法。

我有类似的东西

data (:::) :: Symbol -> * -> * where

data Result = Pre | Post | Match

type family Cmp a b :: Result where
    Cmp (s ::: t) (s ::: t) = Match
    Cmp (s1 ::: t1) (s2 ::: t2) = ???

我想根据CmpSymbolGHC.TypeLits 中的结果返回不同的类型 。感觉就像

Cmp (s1 ::: t1) (s2 ::: t2) = (CmpSymbol s1 s2 ~ LT) => Pre
Cmp (s1 ::: t1) (s2 ::: t2) = (CmpSymbol s1 s2 ~ GT) => Post

应该工作，但它没有。有趣的是，这不是语法错误，而是抱怨它不友善。

我可以通过使用不可判定的实例和辅助函数以某种方式让它工作：

type family Cmp a b :: Result where
    Cmp (s ::: t) (s ::: t) = Match
    Cmp (s1 ::: t1) (s2 ::: t2) = Fun (CmpSymbol s1 s2)

type family Fun r :: Result where
    Fun LT = Pre
    Fun GT = Post

但这感觉相当笨重，肯定有更好的方法吗？ghci 还说 即使是关闭的，:kind! Cmp ("a" ::: Int) ("a" ::: String)也有类型。这是为什么？我也看不到在这里处理普通课程的简单方法？如果的定义类似于Fun 'EQFunFun

class Fun2 o r
instance Fun2 LT Pre
instance Fun2 GT Post

有没有办法以一种很好的方式与类型类交谈，或者我是否仅限于使用其他类型系列，例如Fun？

Answer 1

这确实是唯一的方法，尽管我喜欢定义一些可重用的类型函数（==和If），但在你的情况下它会变成If (CmpSymbol s1 s2 == LT) Pre Post.

不幸的是，没有办法LT -> Pre从像这样的类中获取类型函数Fun2.

你的例子很友善，Fun EQ因为你将CmpSymbol "a" "a"其EQ传递给Fun. 它不只是给出错误的原因是类型族被尽可能晚地评估 - 这里你不要求它的“值”，Fun EQ所以还没有必要评估它。