Skip to content

Instantly share code, notes, and snippets.

View larrytheliquid's full-sized avatar

Larry Diehl larrytheliquid

View GitHub Profile
module FSM where
data Bool : Set where true false : Bool
data List (A : Set) : Set where
[] : List A
_∷_ : A → List A → List A
----------------------------------------------------------------------
module Weed where
data ⊥ : Set where
magic : {A : Set} → ⊥ → A
magic ()
data Weed (A : Set) : Set where
grow : (A → Weed A) → Weed A
@larrytheliquid
larrytheliquid / VecIR.agda
Last active February 26, 2017 23:48
Generic representation: https://is.gd/rms0P7
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
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)
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
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
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".
{-# 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
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
larrytheliquid / Foo.agda
Last active August 29, 2015 13:57
Positivity checker
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))