An idris implementation of well-scoped lambda terms a la Allais et al.

well-scoped.idr

{-
data Λ : List Type -> Type where
  Var : (xs : List Type) -> Λ xs
  Lam : Λ (x :: xs) -> Λ xs
  App : Λ xs -> Λ xs -> Λ xs
-}

Scoped : Type -> Type
Scoped i = i -> List i -> Type

⇒ : (p, q : a -> Type) -> (a -> Type)
⇒ p q = \x => p x -> q x

⊢ : (a -> b) -> (b -> Type) -> (a -> Type)
f `⊢` p = \x => p (f x)

const : Type -> (a -> Type)
const p = \x => p

∀ : (a -> Type) -> Type
∀ p = {x : a} -> p x

data Var : Scoped i where
  z : {σ : i} -> ∀ ((σ ::) `⊢` Var σ)
  s : {σ, τ : i} -> ∀ (Var σ `⇒` ((τ ::) `⊢` Var σ))

data Ty : Type where
  α : Ty
  → : Ty -> Ty -> Ty

data Lam : Scoped Ty where
  var : {σ : Ty} -> ∀ (Var σ `⇒` Lam σ)
  app : {σ, τ : Ty} -> ∀ (Lam (σ `→` τ) `⇒` (Lam σ `⇒` Lam τ))
  lam : {σ, τ : Ty} -> ∀ ((σ ::) `⊢` (Lam τ `⇒` Lam (σ `→` τ)))