agda - 在 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 中保留标签s 指示已对其应用了哪些类型，但随后我必须将自己限制为可标记类型。以前我认为这是唯一的选择，但在依赖类型的土地上似乎发生了很多神奇的事情，我想我会先问。

(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类型和值(value)级别的案例。 GetFn (App f x)然后返回所需的类型和 getFn (App f x)然后返回所需的值。

这里的关键部分是，当你写 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在 Id 中返回案件。

编辑

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