This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Weed where | |
data ⊥ : Set where | |
magic : {A : Set} → ⊥ → A | |
magic () | |
data Weed (A : Set) : Set where | |
grow : (A → Weed A) → Weed A |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 ∙ ε ∶ ℕ ⟩) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module FSM where | |
data Bool : Set where true false : Bool | |
data List (A : Set) : Set where | |
[] : List A | |
_∷_ : A → List A → List A | |
---------------------------------------------------------------------- |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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/ |
OlderNewer