通过利用多个类型类实例之间的对称来缩短代码

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

上述解决方案似乎正确地解决了问题,但它有一个缺点:类型类实例的数量是类型数量的二次方.

题

有什么办法来减少类型的类实例的数量是线性或者通过利用对称性WRT类型的数量,？

可能在这里使用Template Haskell更合适,在这种情况下,请随意建议作为解决方案.

谢谢!

Answer 1

可能有人认为TH在这种情况下更合适.也就是说,无论如何我会用类型来做.

这里的问题是一切都太离散了.您无法遍历前缀以找到正确的前缀,并且您没有表达所需顺序的传递性.我们可以通过任何一种方式解决它.

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

{-# 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

...等等.

现在,要查找较小的前缀,您可以这样做:

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

鉴于此处的所有内容都与类型和驻留在其中的单个nullary构造函数之间存在一对一的对应关系,因此可以使用如下通用类将其转换为术语级别:

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想想为什么.

Fundeps和重叠实例比类型族更强大,但它们整体使用起来比较笨拙,与后者使用的功能性更强的递归样式相比,感觉有点不合适.

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

首先,将所需的顺序作为类型级别列表:

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

使用一些重叠的shenanigans 在类型上实现等式谓词:

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中的上下文减少堆栈非常浅,因此很容易耗尽它并获得类型级别的堆栈溢出(哈哈,是的,这个笑话自己写的)而不是你想要的答案.