Восстановление типа в Идриса

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 бы приветствовать, как хорошо, хотя я предпочел бы Идрис те!)

Answer 1

Конечно. У меня нет компилятор Идриса на этой машине, но здесь это решение в 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) затем возвращает нужный тип и 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 случае.

EDIT

Я думаю, в Идриса вам нужно будет явно квантификации a и b в App конструктора.