Haskell类型促销

Question

我目前正在努力通过48小时写自己的方案,并坚持类型推广.

简而言之,scheme有一个数字塔(Integer-> Rational-> Real-> Complex),具有人们期望的数字促销.我用明显的数字模拟了数字

data Number = Integer Integer | Rational Rational | Real Double | Complex (Complex Double)

所以使用Rank2Types似乎是一种简单的方法,使函数可以在这种类型的范围内工作.对于Num a这个看起来像

liftNum :: (forall a . Num a => a -> a -> a) -> LispVal -> LispVal -> ThrowsError LispVal
liftNum f a b = case typeEnum a `max` typeEnum b of
  ComplexType  -> return . Number . Complex $ toComplex a `f` toComplex b
  RealType     -> return . Number . Real $ toReal a `f` toReal b
  RationalType -> return . Number . Rational $ toFrac a `f` toFrac b
  IntType      -> return . Number . Integer $ toInt a `f` toInt b
  _            -> typeErr a b "Number"

但是很快就会变得冗长,因为每个类型类都需要一个单独的块.
更糟糕的是,Complex的这种实现被简化,因为scheme可以为真实和复杂的部分使用单独的类型.实现这个需要一个自定义版本Number,如果我想避免使类型递归,那么这会使详细程度更糟.

据我所知,没有办法在上下文中进行抽象,所以我希望有一种更简洁的方法来实现这个数字逻辑.

谢谢阅读!

Answer 1

这是一个提案.我们希望你的typeEnum函数做的主要事情还没有将Num a字典纳入范围.因此,让我们使用GADT来实现这一目标.我将简化一些事情,以便更容易解释这个想法并编写代码,但没有必要:我会专注于Number而不是LispVal,当出现问题时我不会报告详细的错误.首先是一些样板:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE Rank2Types #-}
import Control.Applicative
import Data.Complex

现在,您没有给出类型枚举的定义.但是我会给我的,因为它是秘密的一部分:我的类型枚举将通过GADT在Haskell的术语级别和Haskell的类型级别之间建立联系.

data TypeEnum a where
    Integer  :: TypeEnum Integer
    Rational :: TypeEnum Rational
    Real     :: TypeEnum Double
    Complex  :: TypeEnum (Complex Double)

由于这种联系,我的Number类型不需要再次重复这些情况.(我怀疑你TypeEnum和它们的Number类型相互之间是相当重复的.)

data Number where
    Number :: TypeEnum a -> a -> Number

现在我们将定义一个你没有的新类型,它将TypeEnum与Num适当类型的字典绑定在一起.这将是我们typeEnum函数的返回类型.

data TypeDict where
    TypeDict :: Num a => TypeEnum a -> TypeDict

ordering :: TypeEnum a -> Int
ordering Integer  = 0 -- lowest
ordering Rational = 1
ordering Real     = 2
ordering Complex  = 3 -- highest

instance Eq  TypeDict where TypeDict l == TypeDict r = ordering l == ordering r
instance Ord TypeDict where compare (TypeDict l) (TypeDict r) = compare (ordering l) (ordering r)

该ordering函数反映了(我的猜测)强制转换的方向.如果你试图实现Eq与Ord这种类型的自己,没有在我的解决办法偷看,我怀疑你会发现为什么GHC不太愿意获得这些类GADTs.(至少,我花了几次尝试!显而易见的定义没有进行类型检查,而且稍微不那么明显的定义有错误的行为.)

现在我们准备编写一个为数字生成字典的函数.

typeEnum :: Number -> TypeDict
typeEnum (Number Integer  _) = TypeDict Integer
typeEnum (Number Rational _) = TypeDict Rational
typeEnum (Number Real     _) = TypeDict Real
typeEnum (Number Complex  _) = TypeDict Complex

我们还需要铸造功能; 你基本上可以toComplex在这里连接你和朋友的定义:

-- combines toComplex, toFrac, toReal, toInt
to :: TypeEnum a -> Number -> Maybe a
to Rational (Number Integer  n) = Just (fromInteger n)
to Rational (Number Rational n) = Just n
to Rational _ = Nothing
-- etc.
to _ _ = Nothing

一旦我们拥有这种机器,liftNum就会出奇地缩短.我们只需找到要转换的适当类型,获取该类型的字典,然后执行强制转换和操作.

liftNum :: (forall a. Num a => a -> a -> a) -> Number -> Number -> Maybe Number
liftNum f a b = case typeEnum a `max` typeEnum b of
    TypeDict ty -> Number ty <$> liftA2 f (to ty a) (to ty b)

在这一点上你可能会抱怨:你的最终目标是每个类实例没有一个案例liftNum,我们已经实现了这个目标,但看起来我们只是把它推到了定义中typeEnum,每个案例有一个案例类实例.但是,我为自己辩护:你没有向我们展示你的typeEnum,我怀疑每个班级实例已经有一个案例.因此,除了并且确实已经大大简化之外,我们没有在功能上产生任何新的成本.这也为更复杂的操作提供了平滑的升级路径:扩展定义,演员和功能,你很高兴; 可能保持不变.(如果事实证明类型不是线性排序的,而是某种格子或类似的,那么你可以从类中切换.)liftNumliftNumComplexTypeEnumorderingtoliftNumOrd