利用多类型类实例之间的对称性缩短代码

Question

上下文

我正在编写一个表示SI前缀的Haskell模块：

module Unit.SI.Prefix where

每个SI前缀都有相应的数据类型：

data Kilo = Kilo deriving Show
data Mega = Mega deriving Show
data Giga = Giga deriving Show
data Tera = Tera deriving Show

-- remaining prefixes omitted for brevity

问题

我想编写一个函数，当用两个SI前缀应用时，确定静态，其中哪个前缀是更小的。例如：

-- should compile:
test1 = let Kilo = smaller Kilo Giga in ()
test2 = let Kilo = smaller Giga Kilo in ()

-- should fail to compile:
test3 = let Giga = smaller Kilo Giga in ()
test4 = let Giga = smaller Giga Kilo in ()

初始解

下面是一个使用类型类和函数依赖项的解决方案：

{-# LANGUAGE FunctionalDependencies #-}                                                                                         
{-# LANGUAGE MultiParamTypeClasses #-}

class Smaller a b c | a b -> c where smaller :: a -> b -> c

instance Smaller Kilo Kilo Kilo where smaller Kilo Kilo = Kilo
instance Smaller Kilo Mega Kilo where smaller Kilo Mega = Kilo
instance Smaller Kilo Giga Kilo where smaller Kilo Giga = Kilo
instance Smaller Kilo Tera Kilo where smaller Kilo Tera = Kilo

instance Smaller Mega Kilo Kilo where smaller Mega Kilo = Kilo
instance Smaller Mega Mega Mega where smaller Mega Mega = Mega
instance Smaller Mega Giga Mega where smaller Mega Giga = Mega
instance Smaller Mega Tera Mega where smaller Mega Tera = Mega

instance Smaller Giga Kilo Kilo where smaller Giga Kilo = Kilo
instance Smaller Giga Mega Mega where smaller Giga Mega = Mega
instance Smaller Giga Giga Giga where smaller Giga Giga = Giga
instance Smaller Giga Tera Giga where smaller Giga Tera = Giga

instance Smaller Tera Kilo Kilo where smaller Tera Kilo = Kilo
instance Smaller Tera Mega Mega where smaller Tera Mega = Mega
instance Smaller Tera Giga Giga where smaller Tera Giga = Giga
instance Smaller Tera Tera Tera where smaller Tera Tera = Tera

上面的解决方案似乎正确地解决了这个问题，但是它有一个缺点:类型类实例的数量是二次型 w.r.t。类型的数量。

问题

是否有任何方法将类型类实例的数量减少为线性 w.r.t。类型的数量，也许是利用对称性？

在这里使用模板Haskell可能更合适，在这种情况下，可以随意建议将其作为解决方案。

谢谢!

Answer 1

可能有人会说，在这种情况下，这样做更合适。话虽如此，我还是会用类型来做的。

这里的问题是每件事都太离散了。您不能反复遍历前缀以找到正确的前缀，也不能表示所需顺序的传递性。我们可以通过任何一条路线解决这个问题。

对于递归解决方案，我们首先在类型级别创建自然数和布尔值：

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}

data No = No deriving (Show)
data Yes = Yes deriving (Show)

newtype S nat = Succ nat deriving (Show)
data Z = Zero deriving (Show)

type Zero  = Z
type One   = S Zero
type Two   = S One
type Three = S Two

一点简单的算术：

type family Plus x y :: *
type instance Plus x Z = x
type instance Plus Z y = y
type instance Plus (S x) (S y) = S (S (Plus x y))

type family Times x y :: *
type instance Times x Z = Z
type instance Times x (S y) = Plus x (Times y x)

一个“小于或等于”谓词和一个简单的条件函数：

type family IsLTE n m :: *
type instance IsLTE Z Z = Yes
type instance IsLTE (S m) Z = No
type instance IsLTE Z (S n) = Yes
type instance IsLTE (S m) (S n) = IsLTE m n

type family IfThenElse b t e :: *
type instance IfThenElse Yes t e = t
type instance IfThenElse No t e = e

并将SI前缀转换为它们所代表的大小：

type family Magnitude si :: *
type instance Magnitude Kilo = Three
type instance Magnitude Mega = Three `Times` Two
type instance Magnitude Giga = Three `Times` Three

...etc。

现在，要找到较小的前缀，可以这样做：

type family Smaller x y :: *
type instance Smaller x y = IfThenElse (Magnitude x `IsLTE` Magnitude y) x y

既然这里的每一件事在类型和单髓构造函数之间有一对一的对应关系，那么就可以使用这样的泛型类将其转换为术语级：

class TermProxy t where term :: t
instance TermProxy No where term = No
instance TermProxy Yes where term = Yes
{- More instances here... -}

smaller :: (TermProxy a, TermProxy b) => a -> b -> Smaller a b
smaller _ _ = term

根据需要填写详细信息。

另一种方法是使用函数依赖关系和重叠实例来编写通用实例以填补空白--因此您可以为Kilo < Mega、Mega < Giga等编写特定实例，并让它推断这也意味着Kilo < Giga。

这将更深入地将函数依赖视为什么--一种原始的逻辑编程语言。如果你曾经使用过Prolog，你应该有一个粗略的想法。在某些方面，这很好，因为您可以让编译器基于一种更声明性的方法来解决问题。另一方面这也有点可怕因为..。

• 选择实例时不需要查看约束，只有实例头。
• 没有回溯去寻找解决方案。
• 为了表达这类事情，您必须打开UndecidableInstances，因为GHC对于它所知道的将终止的内容非常保守；但是您必须注意不要将类型检查器发送到无限循环中。例如，考虑到像Smaller Kilo Kilo Kilo和(Smaller a s c, Smaller t b s) => Smaller a b c这样的实例，很容易做到这一点--想想为什么。

Fundep和重叠实例严格来说比类型族更强大，但它们在总体上使用起来比较笨拙，与后者使用的功能更强的递归样式相比有些不合适。

哦，为了完整起见，还有第三种方法:这一次，我们滥用重叠实例给我们直接实现递归解决方案的额外力量，而不是通过转换到自然数和使用结构递归。

首先，将所需的排序具体化为类型级别的列表：

data MIN = MIN deriving (Show)
data MAX = MAX deriving (Show)

infixr 0 :<
data a :< b = a :< b deriving (Show)

siPrefixOrd :: MIN :< Kilo :< Mega :< Giga :< Tera :< MAX
siPrefixOrd = MIN :< Kilo :< Mega :< Giga :< Tera :< MAX

在类型上实现一个相等谓词，使用一些重叠的恶作剧：

class (TypeEq' () x y b) => TypeEq x y b where typeEq :: x -> y -> b
instance (TypeEq' () x y b) => TypeEq x y b where typeEq _ _ = term

class (TermProxy b) => TypeEq' q x y b | q x y -> b
instance (b ~ Yes) => TypeEq' () x x b 
instance (b ~ No) => TypeEq' q x y b 

替代类“小于”类，有两个简单的例子：

class IsLTE a b o r | a b o -> r where
    isLTE :: a -> b -> o -> r

instance (IsLTE a b o r) => IsLTE a b (MIN :< o) r where
    isLTE a b (_ :< o) = isLTE a b o

instance (No ~ r) => IsLTE a b MAX r where
    isLTE _ _ MAX = No

然后是递归案例，带有一个辅助类，用于根据类型级布尔值的案例分析推迟递归步骤：

instance ( TypeEq a x isA, TypeEq b x isB
         , IsLTE' a b isA isB o r
         ) => IsLTE a b (x :< o) r where
    isLTE a b (x :< o) = isLTE' a b (typeEq a x) (typeEq b x) o

class IsLTE' a b isA isB xs r | a b isA isB xs -> r where
    isLTE' :: a -> b -> isA -> isB -> xs -> r

instance (Yes ~ r) => IsLTE' a b Yes Yes xs r where isLTE' a b _ _ _ = Yes
instance (Yes ~ r) => IsLTE' a b Yes No xs r where isLTE' a b _ _ _ = Yes
instance (No ~ r) => IsLTE' a b No Yes xs r where isLTE' a b _ _ _ = No
instance (IsLTE a b xs r) => IsLTE' a b No No xs r where
    isLTE' a b _ _ xs = isLTE a b xs

本质上，这需要一个类型级别的列表和两个任意类型，然后遍历列表并返回Yes (如果它找到了第一个类型)，或者返回No (如果它找到第二个类型或到达列表的末尾)。

这实际上是一种错误(你可以看到，如果你想一种或两种类型不在列表中会发生什么)，并且容易失败--像这样的直接递归在GHC中使用一个非常浅的上下文缩减堆栈，所以很容易耗尽它，得到类型级别的堆栈溢出(哈哈，是的，这个笑话是自己写的)而不是你想要的答案。

Answer 2

您可以将您的类型映射为键入级别的自然数，然后使用这些进行比较。这应该是线性的，因为您只需为每个类型指定一个实例，将其映射到相应的数字。

Haskell上的类型算法页面有一些处理类型级自然数的很好的例子。这是个很好的开始。

还要注意的是，已经有流行的维数包在黑客上使用SI单元进行类似的工作。也许值得看看这是如何在他们的代码中实现的。