9

语境

我正在编写一个代表 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

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

问题

有没有办法将类型类实例的数量减少到与类型数量成线性关系，也许是通过利用对称性？

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

谢谢！

4

2 回答 2

7

可能有人认为 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

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

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

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

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 中的上下文减少堆栈很浅，所以很容易耗尽它并得到类型级别的堆栈溢出（哈哈，是的，笑话自己写的）而不是你想要的答案。

于 2011-08-26T16:49:49.887 回答
3

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

Haskell Wiki 上的类型算术页面有一些很好的使用类型级别自然数的示例。这将是一个很好的起点。

另请注意，Hackage 上已经有流行的包尺寸，用于以类似的方式使用 SI 单位。看看这是如何在他们的代码中实现的可能是值得的。

于 2011-08-26T16:42:55.520 回答