larrytheliquid

{-
How does local completeness (http://www.cs.cmu.edu/~fp/courses/15317-f09/lectures/03-harmony.pdf) generalize to eliminators?

Below is the eliminator for `ℕ` that does not include the inductive hypothesis `P n` in the `suc n` branch.
It still passes local completeness because the `suc n` branch still includes the `n` index, it merely omits the inductive hypothesis.

Caveats:
1. `ℕ` is a datatype rather than a standard logical proposition, and it has many proofs/inhabitants for the same type.
2. I'm being more strict here by requiring the expansion to equal the input, rather than merely proving the same proposition.
-}

larrytheliquid

open import Data.Bool
open import Data.Nat
module HypotheticalFunMatching where

{-
Imagine that the expressions in the pattern positions are first evaluated to values/neutrals.
So for example, "not" really becomes elimBool and "_+_" becomes two nested elimℕ's.

A wildcard match is always necessary because there are infinitely many intentionally different
functions.

larrytheliquid

open import Data.Nat
open import Data.String
open import Function
open import LabelledTypes
module LabelledAdd1 where

----------------------------------------------------------------------

add : (m n : ℕ) → ⟨ "add" ∙ m ∙ n ∙ ε ∶ ℕ ⟩
add m n = elimℕ (λ m' → ⟨ "add" ∙ m' ∙ n ∙ ε ∶ ℕ ⟩)

larrytheliquid

λ A m n →
  ind
  (`Arg (Tag ("nil" ∷ "cons" ∷ []))
   (λ t →
      case
      (λ _ →
         Desc
         (μ
          (`Arg (Tag ("zero" ∷ "suc" ∷ []))
           (λ t₁ → case (λ _ → Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))

larrytheliquid

module Foo where
open import Level using ( Lift )

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

elimℕ : ∀{ℓ} (P : ℕ → Set ℓ)
  (pzero : P zero)
  (psuc : (n : ℕ) → P n → P (suc n))

larrytheliquid

There are a lot of resources to learn from, and it's hard to pick just one. Below are links to learning about dependently typed programming. I think that the most comfortable path is to learn DT programming first, and then learn more of the pure math and type theory behind it along the way as you get more experienced.

Basically, Coq is the most mature and oldest, but is more tedious to do dependently typed programming with.
Agda is not as mature, but it supports dependently typed programming very well.
Idris is an even newer language that also supports dependently typed programming well, and IMO has the best chance of being a practically used language.
Personally, I mostly use Agda.

Coq:
Software foundations - http://www.cis.upenn.edu/~bcpierce/sf/toc.html
Certified programming with dependent types - http://adam.chlipala.net/cpdt/

larrytheliquid

{-# OPTIONS --copatterns #-}
module CoList where

{- High-level intuition:

codata CoList (A : Set) : Set where
  nil : CoList A
  cons : A → CoList A → CoList A

append : ∀{A} → CoList A → CoList A → CoList A

larrytheliquid

open import Data.Unit
open import Data.Bool
open import Data.Nat
open import Data.Product
module _ where

{-
This odd approach gives you 2 choices when defining an indexed type:
1. Use a McBride-Dagand encoding so your datatype 
   "need not store its indices".

larrytheliquid

open import Data.Unit
open import Data.Product
module _ where

----------------------------------------------------------------------

data Desc (I : Set) (O : I → Set) : Set₁ where
  `ι : (i : I) (o : O i) → Desc I O
  `δ : (A : Set) (i : A → I) (D : (o : (a : A) → O (i a)) → Desc I O) → Desc I O
  `σ : (A : Set) (D : A → Desc I O) → Desc I O

larrytheliquid

open import Data.Unit
open import Data.Bool
open import Data.Nat
open import Data.Product
module _ where

----------------------------------------------------------------------

data Desc (I : Set) : Set₁ where
  `ι : I → Desc I