主页 / user-9759263

F. Zer's questions

Martin Hope
F. Zer
Asked: 2025-01-12 22:26:00 +0800 CST
  • 6

我一直在深入研究foldTreeHaskell中的函数，它的定义如下：

foldTree :: (a -> [b] -> b) -> Tree a -> b
foldTree f = go where
    go (Node x ts) = f x (map go ts)

最近我偶然发现了对这句话的如下解释：

当我们调用时f x vs，我们假设x和vs已经与已知值绑定。

go (Node x ts) = f x (map go ts)
  • 的值x已经按照预期且熟悉的方式进行绑定。
  • 然而，尚未绑定任何值vs；绑定vs被推迟到整个子林的递归完成为止。

提到时间元素（使用“已经”和“尚未”等术语）让我感到困惑。为了更好地理解这一点，我开始尝试一些从自然演绎和归纳证明中借用的概念。具体来说，我试图将第二个论点概念化f如下：

  1. 我假设已经定义了一种类型[b]。
  2. 然后，我考虑的实际定义是将这个假定类型与类型f相结合来定义整体表达式，其中类型为。[b]afoldTree f treetreeTree a

我如何才能在假设方面完善这种思路，而不是使用实际函数求值，假设它是正确的？或者，我是否可以采用另一种正式或直观的视角来更好地理解这个函数及其机制？

haskell
Martin Hope
F. Zer
Asked: 2024-04-24 20:52:25 +0800 CST
  • 7

出于学习目的，我用gcd'重复减法来定义函数：

gcd' :: Integer -> Integer -> Integer
gcd' x y 
    | x == y = x
    | x < y = gcd' x (y - x)
    | y < x = gcd' (x - y) y

（Prelude的gcd功能）

问题是 GHC 抱怨它：

模式匹配并非详尽无遗。在‘gcd’的方程中：

“Integer”、“Integer”类型的模式不匹配：_ _

我见过一条关于数字的数学定律：

对于所有数字 𝑥 和 𝑦，𝑥 小于 𝑦，或 𝑦 小于 𝑥，或 𝑥 等于 𝑦。

从这个意义上来说，这三个守卫涵盖了所有可能的情况。为什么 GHC 关注这个定义？

haskell
Martin Hope
F. Zer
Asked: 2023-11-21 02:19:26 +0800 CST
  • 6

我尝试State使用类liftIO中的函数在 monad 内打印MonadIO：

import Control.Monad.State
import Control.Monad.IO.Class

import Control.Applicative

facHelper :: Integer -> State Integer ()
facHelper 0 = pure ()
facHelper n = do
  currentState <- get
  liftIO $ putStrLn $ "n = " ++ show currentState
  modify (*n)
  facHelper (n-1)

factorial :: Integer -> Integer
factorial n = snd (runState (facHelper n) 1)

main :: IO ()
main = print $ factorial 6

但是，我收到错误：

没有因使用“liftIO”而产生的 (MonadIO Data.Functor.Identity.Identity) 实例

如果我查找MonadIO班级：

我看到一个例子：

MonadIO m => MonadIO (StateT s m)

并且还看到这State s是一个类型别名

type State s = StateT s Identity

所以，原则上，我可以使用liftIOwith State。哪里有问题 ？

haskell