larrytheliquid

module FSM where

data Bool : Set where true false : Bool

data List (A : Set) : Set where
  [] : List A
  _∷_ : A → List A → List A

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

larrytheliquid

module Weed where

data ⊥ : Set where

magic : {A : Set} → ⊥ → A
magic ()

data Weed (A : Set) : Set where
  grow : (A → Weed A) → Weed A

larrytheliquid

open import Data.Nat
open import Data.Product
open import Data.String
open import Relation.Binary.PropositionalEquality
module _ where

mutual
  data Vec₁ (A : Set) : Set where
    nil : Vec₁ A
    cons : (n : ℕ) → A → (xs : Vec₁ A) → Vec₂ xs ≡ n → Vec₁ A

larrytheliquid

open import Data.Nat
open import Data.Fin renaming ( zero to here ; suc to there )
open import Data.Product
open import Relation.Binary.PropositionalEquality
module _ where

mutual
 data Vec₁ (A : Set) : ℕ → Set where
   nil₁ : Vec₁ A zero
   cons₁ : {n : ℕ} → A → (xs : Vec₁ A n) → toℕ (Vec₂ xs) ≡ n → Vec₁ A (suc n)

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

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

{-
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

{-# 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

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

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))