如何实现`Constraint`反射?[基于可用约束的特殊多态性]

huangapple go评论61阅读模式
英文:

How to implement `Constraint` reflection? [Ad-Hoc polymorphism based on available Constraints]

问题

例如,使用类型,您可以使用 Typeable 来实现自定义多态,根据输入类型的不同定义不同的行为:

foo :: forall a. Typeable a => a -> a
foo | Just HRefl <- typeRep @a `eqTypeRep` typeRep @Bool = not
    | otherwise = id

-- >>> foo 3
3
-- >>> foo True
False

我想要做类似的事情,但是检查类型是否具有 Constraint 的特定实例,并根据情况实施不同的行为。

到目前为止,我已经查看了两个包,Data.ConstraintData.Exists。我认为解决方案可能在其中一个中,但我还没有弄清楚如何去做。

为了了解背景,这是在我考虑多态安全整数除法函数会是什么样子时产生的:

polymorphicSafeDiv :: Integral a => a -> a -> Maybe a
polymorphicSafeDiv x y = undefined

如果我希望这个函数对有界和无界的 Integral 都有效,我需要考虑除零和 minBound @Int / (-1) 的溢出情况。我会想象这样:

polymorphicSafeDiv :: Integral a => a -> a -> Maybe a
polymorphicSafeDiv x y
 | y == 0    = Nothing
 | y == (-1) = case (???) of
                 Just Relf -> Nothing
                 _         -> Just $ x `div` y
 | otherwise = Just $ x `div` y
英文:

For example, with types, you can implement AdHoc polymorphism using Typeable to define a different behavior depending on what the input type is:

foo :: forall a. Typeable a =&gt; a -&gt; a
foo | Just HRefl &lt;- typeRep @a `eqTypeRep` typeRep @Bool = not
    | otherwise = id

-- &gt;&gt;&gt; foo 3
3
-- &gt;&gt;&gt; foo True
False

I would like to do something similar to that but instead check if a type has a curtain instance of a Constraint, and implement a different behavior on that.

So far I have looked at two packages, Data.Constraint and Data.Exists. I think the solution lies with one of them but I have not been able to understand how I would go about doing this.

For context, this came about when I was thinking about what a polymorphic safe integer division function would look like

polymorphicSafeDiv :: Integral a =&gt; a -&gt; a -&gt; Maybe a
polymorphicSafeDiv x y = undefined

If I want this function to work for both bounded and unbounded Integrals I need to consider both, division by zero, and the overflow scenario for minBound @Int / (-1). I would imagine something like

polymorphicSafeDiv :: Integral a =&gt; a -&gt; a -&gt; Maybe a
polymorphicSafeDiv x y
 | y == 0    = Nothing
 | y == (-1) = case (???) of
                 Just Relf -&gt; Nothing
                 _         -&gt; Just $ x `div` y
 | otherwise = Just $ x `div` y

答案1

得分: 2

使用评论中建议的 if-instance,可以以非常人性化的方式表达我想要的内容,尽管任何调用代码也需要打开扩展。

{-# OPTIONS_GHC -fplugin=IfSat.Plugin #-}

module Main where

import Data.Constraint.If (IfSat, ifSat)

polymorphicSafeDiv :: forall a. (IfSat (Bounded a), Integral a) => a -> a -> Maybe a
polymorphicSafeDiv x y
  | y == 0 = Nothing
  | otherwise = ifSat @(Bounded a) boundedSafeDiv optmisticDiv
  where
    optmisticDiv = Just $ x `div` y

    boundedSafeDiv :: (Bounded a, Integral a) => Maybe a
    boundedSafeDiv
      | y == minBound `quot` maxBound = if x == minBound then Nothing else optmisticDiv
      | otherwise = optmisticDiv

main :: IO ()
main = do
  print (polymorphicSafeDiv (minBound @Int) (-1))
  print (polymorphicSafeDiv (minBound @Int) (-2))
  print (polymorphicSafeDiv (minBound @Int) 0)
  print (polymorphicSafeDiv (minBound @Word) 0)
  print (polymorphicSafeDiv (minBound @Word) maxBound)
  print (polymorphicSafeDiv (2 ^ 128) (-1))
  print (polymorphicSafeDiv (2 ^ 128) 0)

{- Nothing
Just 4611686018427387904
Nothing
Nothing
Just 0
Just (-340282366920938463463374607431768211456)
Nothing -}
英文:

Using the if-instance as suggested in the comments leads to a very ergonomic way to express what I wanted, although any calling code will need the extension turned on as well

{-# OPTIONS_GHC -fplugin=IfSat.Plugin #-}

module Main where

import Data.Constraint.If ( IfSat, ifSat )

polymorphicSafeDiv :: forall a. (IfSat (Bounded a), Integral a) =&gt; a -&gt; a -&gt; Maybe a
polymorphicSafeDiv x y 
  | y == 0    = Nothing
  | otherwise = ifSat @(Bounded a) boundedSafeDiv optmisticDiv
  where
    optmisticDiv = Just $ x `div` y 

    boundedSafeDiv :: (Bounded a, Integral a) =&gt; Maybe a
    boundedSafeDiv
      | y == minBound `quot` maxBound = if x == minBound then Nothing else optmisticDiv
      | otherwise                     = optmisticDiv

main :: IO ()
main = do 
  print (polymorphicSafeDiv (minBound @Int ) (-1))
  print (polymorphicSafeDiv (minBound @Int ) (-2))
  print (polymorphicSafeDiv (minBound @Int ) 0   )
  print (polymorphicSafeDiv (minBound @Word) 0   )
  print (polymorphicSafeDiv (minBound @Word) maxBound)
  print (polymorphicSafeDiv (2^128)          (-1))
  print (polymorphicSafeDiv (2^128)          0   )

{-
Nothing
Just 4611686018427387904
Nothing
Nothing
Just 0
Just (-340282366920938463463374607431768211456)
Nothing
-}

答案2

得分: 1

做这个的惯用方法是创建一个新的类。

    class LowerBound a where lowerBound :: Maybe a
    instance LowerBound Int where lowerBound = Just minBound
    instance LowerBound Integer where lowerBound = Nothing

    polymorphicSafeDiv :: (LowerBound a, Integral a) => a -> a -> Maybe a
    polymorphicSafeDiv x = \case
        0  -> Nothing
        -1 -> case lowerBound of
            Just lb | x == lb -> Nothing
            _ -> Just (x `div` y)
        y  -> Just (x `div` y)

实际上,我不确定 `LowerBound` 是一个很好的名称。例如,`Word` 有一个下限,但将其除以其他数不应产生 `Nothing`。也许你应该直接创建一个除法类。

    class Integral a => SafeDivide a where
        safeDiv :: a -> a -> Maybe a
        default safeDiv :: Bounded a => a -> a -> Maybe a
        safeDiv x = \case
            -1 | x == minBound -> Nothing
            y -> testZeroDiv x y

    testZeroDiv :: Integral a => a -> a -> Maybe a
    testZeroDiv x = \case
        0 -> Nothing
        y -> Just (x `div` y)

    instance SafeDivide Int
    instance SafeDivide Integer where safeDiv = testZeroDiv
    instance SafeDivide Word where safeDiv = testZeroDiv
英文:

The idiomatic way to do this is to make a new class.

class    LowerBound a       where lowerBound :: Maybe a
instance LowerBound Int     where lowerBound = Just minBound
instance LowerBound Integer where lowerBound = Nothing

polymorphicSafeDiv :: (LowerBound a, Integral a) =&gt; a -&gt; a -&gt; Maybe a
polymorphicSafeDiv x = \case
    0  -&gt; Nothing
    -1 -&gt; case lowerBound of
        Just lb | x == lb -&gt; Nothing
        _ -&gt; Just (x `div` y)
    y  -&gt; Just (x `div` y)

Actually, I'm not sure LowerBound is a great name for this. For example, Word has a lower bound, but dividing it by other things shouldn't produce Nothing. Perhaps you should make a division class directly.

class Integral a =&gt; SafeDivide a where
    safeDiv :: a -&gt; a -&gt; Maybe a
    default safeDiv :: Bounded a =&gt; a -&gt; a -&gt; Maybe a
    safeDiv x = \case
        -1 | x == minBound -&gt; Nothing
        y -&gt; testZeroDiv x y

testZeroDiv :: Integral a =&gt; a -&gt; a -&gt; Maybe a
testZeroDiv x = \case
    0 -&gt; Nothing
    y -&gt; Just (x `div` y)

instance SafeDivide Int
instance SafeDivide Integer where safeDiv = testZeroDiv
instance SafeDivide Word    where safeDiv = testZeroDiv

huangapple
  • 本文由 发表于 2023年2月18日 22:07:52
  • 转载请务必保留本文链接:https://go.coder-hub.com/75493880.html
匿名

发表评论

匿名网友

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen:

确定