haskell - Agda:我的代码没有类型检查(如何正确获取隐式参数？)

“checkSimple”获取u，它是Universe U的元素，并检查是否
(nat 1)可以转换为给定u的agda类型。返回转换结果。

现在，我尝试编写一个控制台程序，并从命令行获取“someU”。

因此，我更改了“checkSimple”的类型，以包含一个(u:也许是U)作为参数(可能是因为控制台的输入可能为“nothing”)。但是我无法获取代码以进行检查。

module CheckMain where


open import Prelude

-- Install Prelude
---- clone this git repo:
---- https://github.com/fkettelhoit/agda-prelude

-- Configure Prelude
--- press Meta/Alt and the letter X together
--- type "customize-group" (i.e. in the mini buffer)
--- type "agda2"
--- expand the Entry "Agda2 Include Dirs:"
--- add the directory



data S : Set where
  nat  : (n : ℕ) → S
  nil  : S

sToℕ : S → Maybe ℕ
sToℕ (nat n) = just n
sToℕ _       = nothing


data U : Set where
  nat     : U

El : U → Set
El nat = ℕ


sToStat : (u : U) → S → Maybe (El u)
sToStat nat           s = sToℕ s


-- Basic Test
test1 : Maybe ℕ
test1 = sToStat nat (nat 1)


{- THIS WORKS -}

checkSimple : (u : U) → Maybe (El u)
checkSimple someU = sToStat someU (nat 1)



{- HERE IS THE ERROR -}

-- in contrast to checkSimple we only get a (Maybe U) as a parameter
-- (e.g. from console input)

check : {u : U} (u1 : Maybe U) → Maybe (El u)
check (just someU) = sToStat someU (nat 1)
check _ = nothing


{- HER IS THE ERROR MESSAGE -}

{-
someU != .u of type U
when checking that the expression sToStat someU (nat 1) has type
Maybe (El .u)
-}

最佳答案

问题本质上很简单:sToStat的最终类型取决于其第一个参数的值(代码中的u : U)。以后当您在sToStat中使用check时，您希望返回类型取决于someU-但check promise 其返回类型取决于隐式u : U!

现在，让我们想象一下它确实进行了类型检查，我将向您展示一些可能出现的问题。

如果u1是nothing怎么办？好吧，在这种情况下，我们也想返回nothing。什么类型的nothing？您可能会说Maybe (El u)，但这就是问题-u被标记为隐式参数，这意味着编译器将尝试从其他上下文中为我们推断出它。但是没有其他上下文可以限制u的值!

每当您尝试使用check时，Agda极有可能提示 Unresolved 元变量，这意味着您必须在所有使用u的地方都写入check的值，这样就打败了首先标记隐式u的观点。万一您不知道，Agda为我们提供了一种提供隐式参数的方法:

check {u = nat} {- ... -}

但是我离题了。

如果使用更多构造函数扩展U，则另一个问题变得显而易见:

data U : Set where
    nat char : U

例如。我们还必须在其他几个函数中考虑这种额外的情况，但是出于本示例的目的，我们只需要:

El : U → Set
El nat  = ℕ
El char = Char

现在，check {u = char} (just nat)是什么？ sToStat someU (nat 1)是Maybe ℕ，但是El u是Char!

现在为可能的解决方案。我们需要使check的结果类型某种程度上取决于u1。如果我们有某种unJust函数，我们可以编写

check : (u1 : Maybe U) → Maybe (El (unJust u1))

您应该立即看到此代码的问题-不能保证我们u1是just。即使我们要返回nothing，我们仍然必须提供正确的类型!

首先，我们需要为nothing情况选择某种类型。假设我想稍后扩展U，所以我需要选择中性的东西。 Maybe ⊤听起来很合理(提醒一下，⊤是Haskell中()的含义-单位类型)。

在某些情况下，如何使check返回Maybe ℕ，而在另一些情况下，如何返回Maybe ⊤？啊，我们可以使用一个函数!

Maybe-El : Maybe U → Set
Maybe-El nothing  = Maybe ⊤
Maybe-El (just u) = Maybe (El u)

这正是我们所需要的!现在check变成:

check : (u : Maybe U) → Maybe-El u
check (just someU) = sToStat someU (nat 1)
check nothing      = nothing

同样，这是提及这些功能的简化行为的绝好机会。 Maybe-El在这方面不是很理想，让我们看一下另一个实现并做一些比较。

Maybe-El₂ : Maybe U → Set
Maybe-El₂ = Maybe ∘ helper
  where
    helper : Maybe U → Set
    helper nothing  = ⊤
    helper (just u) = El u

或者，也许我们可以为我们节省一些输入并编写:

Maybe-El₂ : Maybe U → Set
Maybe-El₂ = Maybe ∘ maybe El ⊤

好吧，从它们为相同输入给出相同答案的意义上讲，以前的Maybe-El和新的Maybe-El₂是等效的。即∀ x → Maybe-El x ≡ Maybe-El₂ x。但是有一个巨大的区别。如果不查看Maybe-El x是什么，我们能告诉x吗？是的，我们什么也不能说。在继续之前，这两个函数用例都需要了解有关x的知识。

但是Maybe-El₂呢？让我们尝试相同的方法:我们从Maybe-El₂ x开始，但是这次，我们可以应用(唯一的)函数案例。展开一些定义，我们得出:

Maybe-El₂ x ⟶ (Maybe ∘ helper) x ⟶ Maybe (helper x)

现在我们陷入困境，因为要减少helper x，我们需要知道x是什么。但是，看，我们比Maybe-El更远了。这有什么不同吗？

考虑一下这个非常愚蠢的功能:

discard : {A : Set} → Maybe A → Maybe ⊤
discard _ = nothing

当然，我们希望以下函数能够进行类型检查。

discard₂ : Maybe U → Maybe ⊤
discard₂ = discard ∘ check

check正在为某些Maybe y生成y，对不对？嗯，问题来了-我们知道check x : Maybe-El x，但是我们对x一无所知，所以我们也不能假设Maybe-El x也可以简化为Maybe y!

在Maybe-El₂方面，情况完全不同。我们知道Maybe-El₂ x简化为Maybe y，因此discard₂现在进行类型检查!

关于haskell - Agda:我的代码没有类型检查(如何正确获取隐式参数？)，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/12097474/