Agda:我的代码没有键入检查(如何获取隐式参数？)

Question

"checkSimple"获取宇宙U的元素u,并检查是否(nat 1)可以转换为给定u的agda类型.返回转换结果.

现在我尝试编写一个控制台程序并从命令行获取"someU".

因此,我将"checkSimple"的类型更改为包含(u:Maybe U)作为参数(可能因为来自控制台的输入可以是"无").但是我无法获取键入检查的代码.

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)
-}

Answer 1

问题本质上非常简单:结果类型sToStat取决于其第一个参数的值(u : U在您的代码中); 当你以后使用sToStatinside时check,你希望返回类型依赖someU- 但是check承诺它的返回类型取决于隐式u : U!

现在,让我们想象一下这样做,我会告诉你几个问题.

如果u1是的话nothing？那么,在这种情况下我们也希望返回nothing.nothing什么类型的？Maybe (El u)你可能会说,但这里的东西 - u标记为隐式参数,这意味着编译器会尝试从其他上下文中为我们推断它.但没有其他背景可以降低价值u!

无论何时尝试使用check,Agda都很可能会抱怨未解决的元变量,这意味着你必须写下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?现在typechecks!