主页 / user-10432645

Joris KBos's questions

Martin Hope
Joris KBos
Asked: 2025-04-17 02:30:49 +0800 CST
  • 7

我对 Agda 很熟悉。我决定尝试一下 Lean，但我发现命题相等性真的让我很困扰。有时候我发现 rfl 能正常工作，但有时候却不行，原因我完全不明白，这真让人沮丧。举个例子：

inductive Λ where
  | var : String → Λ
  | app : Λ → Λ → Λ
  | abs : String → Λ → Λ
  deriving Repr, BEq, DecidableEq

def FV : Λ → HashSet String
  | Λ.var x => HashSet.ofList [x]
  | Λ.app m n  => FV m ∪ FV n
  | Λ.abs x m => (FV m).erase x
  
#eval FV (Λ.var "x")  -- Std.HashSet.ofList ["x"]
example : FV (Λ.var "x") = HashSet.ofList ["x"] := rfl  -- fine
example : (2 == 1 + 1) = true := rfl -- fine
#eval FV (Λ.var "x") == HashSet.ofList ["x"]  -- true
example : (FV (Λ.var "x") == HashSet.ofList ["x"]) = true := rfl
--type mismatch
--  rfl
--has type
--  ?m.9390 = ?m.9390 : Prop
--but is expected to have type
--  (FV (Λ.var "x") == HashSet.ofList ["x"]) = true : Prop

表达式的计算结果与预期一致，但在前两个例子中， rfl 运行良好，但在最后一个例子中却莫名其妙地不行，似乎没有减少 = 两边的项。我可以想象两个具有相同值的 HashSet 并不总是相等，因为它们可能最终位于不同的 bucket 中，但我不确定这是否是问题所在，因为它的计算结果似乎很好。

functional-programming
Martin Hope
Joris KBos
Asked: 2023-12-31 04:00:59 +0800 CST
  • 5

在 Haskell 中，我习惯在函数上使用 liftA2 作为 S' 组合器。这是有效的，因为 Haskell STL 实例化了函数的 Functor 和 Applicative（请参阅 https://hackage.haskell.org/package/base-4.12.0.0/docs/src/GHC.Base.html#line-818）。据我所知，Idris STL 并没有这样做（除了我在 STL 中也找不到 liftA2 的事实），所以我想我应该自己做。只是，它似乎不起作用，但也许我对伊德里斯不够了解，因为我今天才第一次尝试。

我能够实例化 \b => a -> b 的 Functor 和 Applicative，但是类型系统似乎无法弄清楚当我使用 a -> b 类型的东西时，applicative functor 应该是 \b => a -> b。

我有以下代码：

Functor (\b => a -> b) where
  map = (.)

Applicative (\b => a -> b) where
  pure = const
  (<*>) f g x = f x (g x)

liftA2 : (Functor f, Applicative f) => (a -> b -> c) -> f a -> f b -> f c
liftA2 = (<*>) .: map

S' : (b -> c -> d) -> (a -> b) -> (a -> c) -> a -> d
S' = liftA2

但 S' 的定义给出了以下错误：

Error: While processing right hand side of S'. Can't find an implementation for (Functor ?f, Applicative ?f).

Helpers:16:6--16:12
 12 | liftA2 : (Functor f, Applicative f) => (a -> b -> c) -> f a -> f b -> f c
 13 | liftA2 = (<*>) .: map
 14 |
 15 | S' : (b -> c -> d) -> (a -> b) -> (a -> c) -> a -> d
 16 | S' = liftA2
           ^^^^^^
functor