Skip to content

Instantly share code, notes, and snippets.

Larry Diehl larrytheliquid

View GitHub Profile
View FSM.agda
module FSM where
data Bool : Set where true false : Bool
data List (A : Set) : Set where
[] : List A
_∷_ : A List A List A
----------------------------------------------------------------------
View Weed.agda
module Weed where
data : Set where
magic : {A : Set} A
magic ()
data Weed (A : Set) : Set where
grow : (A Weed A) Weed A
View VecIR.agda
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
View VecIIR.agda
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)
View General.agda
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
View SafeGenerallyIndexedIR.agda
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
View GenerallyIndexed.agda
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".
View CoList.agda
{-# 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
View gist:1b433ee3a36156a9be42
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 Aug 29, 2015
Positivity checker
View Foo.agda
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))
You can’t perform that action at this time.