在 Idris 中恢复类型

Question

假设我有一个数据类型：

data Term : Type -> Type where
  Id : Term (a -> a)
  ...
  App : Term (a -> b) -> Term a -> Term b

证明是App:

data So : Bool -> Type where 
  Oh : So True

isApp : Term a -> Bool
isApp (App x y) = True
isApp x         = False

是否可以编写一个函数来获取 App 的第一个参数？我不知道如何输入它，因为原始参数类型丢失了：

getFn : (x : Term b) -> So (isApp x) -> ???
getFn (App f v) p = f

我可以在 Term 中保留标签以指示应用了哪些类型，但我必须将自己限制为可标记类型。以前我假设这是唯一的选择，但在依赖类型的领域似乎发生了很多神奇的事情，我想我会先问一下。

（也欢迎使用 Agda 示例，但我更喜欢 Idris 示例！）

Answer 1

当然可以。我在这台机器上没有 Idris 编译器，但是这里有一个 Agda 中的解决方案：

open import Data.Bool.Base

data Term : Set -> Set₁ where
  Id : ∀ {a} -> Term (a -> a)
  App : ∀ {a b} -> Term (a -> b) -> Term a -> Term b

data So : Bool -> Set where 
  Oh : So true

isApp : ∀ {a} -> Term a -> Bool
isApp (App x y) = true
isApp x         = false

GetFn : ∀ {b} -> (x : Term b) -> So (isApp x) -> Set₁
GetFn  Id               ()
GetFn (App {a} {b} f x) _  = Term (a -> b)

getFn : ∀ {b} -> (x : Term b) -> (p : So (isApp x)) -> GetFn x p
getFn  Id       ()
getFn (App f v) p  = f

您只需要在类型和值级别显式丢弃 Id 个案例。 GetFn (App f x) 然后 returns 所需的类型和 getFn (App f x) 然后 returns 所需的值。

这里关键的一点是，当你写getFn (App f v)时，x统一为App f v，类型签名变成GetFn (App f v) p，简化为Term (a -> b) ] 为适当的 a 和 b，这正是 f.

的类型

或者你可以写

GetFn : ∀ {b} -> Term b -> Set₁
GetFn  Id               = junk where junk = Set
GetFn (App {a} {b} f x) = Term (a -> b)

getFn : ∀ {b} -> (x : Term b) -> So (isApp x) -> GetFn x
getFn  Id       ()
getFn (App f v) p  = f

getFn 丢弃 Id，所以我们不关心 GetFn returns 在 Id 情况下的垃圾。

编辑

我想在 Idris 中，您需要在 App 构造函数中显式量化 a 和 b。

在 Idris 中恢复类型

Recovering a type in Idris

agda

dependent-type

idris