idris 是否支持一种将对称语句折叠成一个的方法？

Question

我是函数式编程的新手，因此正在学习“使用 Idris 进行类型驱动开发”。 给出一个函数 maxMaybe 可以计算两个 Maybe Double 之间的最大值，定义如下

maxMaybe : Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe Nothing y = y
maxMaybe x Nothing = x
maxMaybe Nothing Nothing = Nothing
maxMaybe (Just x) (Just y) = Just (max x y)

有没有办法将以下案例合并为一个，因为位置并不重要？

maxMaybe Nothing y = y
maxMaybe x Nothing = x

我也很想知道这种事情是否通常在其他纯函数式编程语言（如 Haskell 或 OCaml）中处理

maxMaybe : Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe Nothing y = y
-- maxMaybe x Nothing = x
maxMaybe Nothing Nothing = Nothing
maxMaybe (Just x) (Just y) = Just (max x y)

maxMaybe（仅 5）（无） maxMaybe (Just 5) Nothing : Maybe Integer

Answer 1

你可以写

maxMaybe : Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe mx my = [| max mx my |] <|> mx <|> my

但是在运行时它可能会更昂贵，因为你会重做 除非有足够的编译器优化，否则大量案例分析 给你一些本质上等同于你的东西 原始解决方案。

Answer 2

在 Haskell 中，一个想法可能是使用

Min

半群并换行使用：

import Data.Function (on)
import Data.Semigroup (Max (Max, getMax))

maxMaybe :: Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe = on ((fmap getMax .) . (<>)) (fmap Max)

您可以轻松地将其推广到任何类似结构：

Semigroup

那么 

semiFunc :: (Functor f, Semigroup (f b)) => (a -> b) -> (b -> c) -> f a -> f a -> f c
semiFunc f g = on ((fmap g .) . (<>)) (fmap f)

是

maxMaybe

与

semiFunc

的特例。