Recovering a type in Idris

Question

Let's say I have a datatype:

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

With a proof something is App:

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

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

Is it possible to write a function that gets the first argument of an App? I don't know how I'd type it, since the original argument type is lost:

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

I could keep tags inside the Terms indicating what types have been applied to it, but then I'd have to restrict myself to taggable types. Previously I'd have assume that's the only option, but so many magical things seems to happen in the land of dependent types that I thought I'd ask first.

(Agda examples would be welcome as well, though I'd prefer Idris ones!)

Answer 1

Sure. I don't have an Idris compiler on this machine, but here is a solution in 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

You just need to explicitly discard the Id cases at the type and value levels. GetFn (App f x) then returns the desired type and getFn (App f x) then returns the desired value.

The crucial part here is that when you write getFn (App f v) x gets unified with App f v, the type signature becomes GetFn (App f v) p, which simplifies to Term (a -> b) for the appropriate a and b, which is exactly the type of f.

Alternatively you can write

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 discards Id, so we don't care about junk that GetFn returns in the Id case.

EDIT

I guess in Idris you will need to explicitly quantify over a and b in the App constructor.