|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
-- This file:
-- http://angg.twu.net/IDRIS/Tut.idr.html
-- http://angg.twu.net/IDRIS/Tut.idr
-- (find-angg "IDRIS/Tut.idr")
--
-- This is my eev-ized version of the Idris tutorial. See:
-- http://angg.twu.net/emacsconf2019.html <- eev @ EmacsConf 2019
-- http://angg.twu.net/#eev
-- (find-eev-quick-intro)
--
-- To install Idris on Debian, follow these instructions:
-- (find-es "idris" "idris-on-debian")
-- and add ~/.cabal/bin to the PATH:
-- (find-es "haskell" "cabal-PATH")
--
-- To download Idris from git and compile its documentation into PDFs, do:
-- (find-es "idris" "idris-git")
-- (find-es "idris" "idris-git" "make user_doc_pdf")
-- We will get a file "idris-documentation-complete.pdf".
-- Here's how I use it:
-- (find-pdf-like-intro)
-- (find-angg ".emacs" "idris")
-- (find-es "idris" "idris-doc-complete")
-- See also:
-- (find-es "idris" "idris-docs-online")
--
-- To install idris-mode for Emacs and also download it from git:
-- (find-es "idris" "idris-mode-git")
-- Its main keys (IMHO) are `C-c C-l' and `C-c C-t':
-- https://github.com/idris-hackers/idris-mode
-- (find-idrismodegitfile "readme.markdown" "C-c C-l")
-- (find-idrismodegitfile "readme.markdown" "C-c C-t")
--
-- Note: I know VERY LITTLE Idris at the moment! See:
-- http://angg.twu.net/math-b.html#notes-yoneda
-- (find-TH "math-b" "notes-yoneda")
-- «.import» (to "import")
-- «.types-and-functions» (to "types-and-functions")
-- «.data-types» (to "data-types")
-- «.functions» (to "functions")
-- «.dependent-types» (to "dependent-types")
-- «.useful-data-types» (to "useful-data-types")
-- «.records» (to "records")
-- «.more-expressions» (to "more-expressions")
-- «.interfaces» (to "interfaces")
-- «.theorem-proving» (to "theorem-proving")
--
-- «.Pair» (to "Pair")
-- «import» (to ".import")
-- (find-es "idris" "import")
import public Data.Vect
-- «types-and-functions» (to ".types-and-functions")
-- (find-idrisdoccpage (+ 1 4) "1.3 Types and Functions")
-- (find-idrisdocctext (+ 1 4) "1.3 Types and Functions")
-- (find-idrisdoccpage (+ 1 4) "1.3.1 Primitive Types")
-- (find-idrisdocctext (+ 1 4) "1.3.1 Primitive Types")
-- «data-types» (to ".data-types")
-- (find-idrisdoccpage (+ 1 5) "1.3.2 Data Types")
-- (find-idrisdocctext (+ 1 5) "1.3.2 Data Types")
-- (find-idrisdoccpage (+ 1 172) "Data types")
-- (find-idrisdocctext (+ 1 172) "Data types")
data MyNat = Z | S MyNat -- Natural numbers
data MyList a = Nil | (::) a (MyList a) -- Polymorphic lists
{-
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
idris2 Tut.idr
:?
MyNat
Z
Main.Z
:r
-- Can't disambiguate name: Main.Z, Prelude.Nat.Z
-- (find-idrisdoccpage (+ 1 221) "6.20.2 Namespaces and type-directed disambiguation")
-- (find-idrisdocctext (+ 1 221) "6.20.2 Namespaces and type-directed disambiguation")
-}
-- «functions» (to ".functions")
-- (find-idrisdoccpage (+ 1 6) "1.3.3 Functions")
-- (find-idrisdocctext (+ 1 6) "1.3.3 Functions")
-- Unary addition
myplus : Nat -> Nat -> Nat
myplus Z y = y
myplus (S k) y = S (myplus k y)
-- Unary multiplication
mymult : Nat -> Nat -> Nat
mymult Z y = Z
mymult (S k) y = myplus y (mymult k y)
{-
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
idris2 Tut.idr
:?
myplus (S (S Z)) (S (S Z))
mymult (S (S (S Z))) (myplus (S (S Z)) (S (S Z)))
(S (S (S (S Z))))
(Main.S (S (S (S Z))))
myplus 2 2
mymult 3 (myplus 2 2)
-}
-- (find-idrisdoccpage (+ 1 7) "where clauses")
-- (find-idrisdocctext (+ 1 7) "where clauses")
reverse : List a -> List a
reverse xs = revAcc [] xs where
revAcc : List a -> List a -> List a
revAcc acc [] = acc
revAcc acc (x :: xs) = revAcc (x :: acc) xs
{-
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
idris2 Tut.idr
:?
[2, 3, 4]
reverse [2, 3, 4]
-}
-- (find-idrisdoccpage (+ 1 7) "Note: Scope")
-- (find-idrisdocctext (+ 1 7) "Note: Scope")
-- foo : Int -> Int
-- foo x = case isLT of
-- Yes => x*2
-- No => x*4
-- where
-- data MyLT = Yes | No
-- isLT : MyLT
-- isLT = if x < 20 then Yes else No
{-
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
idris2 Tut.idr
:?
foo 19 --> 38
foo 20 --> 80
-}
-- «dependent-types» (to ".dependent-types")
-- (find-idrisdoccpage (+ 1 8) "1.3.4 Dependent Types")
-- (find-idrisdocctext (+ 1 8) "1.3.4 Dependent Types")
-- (find-idrisdoccpage (+ 1 9) "Vectors")
-- (find-idrisdocctext (+ 1 9) "Vectors")
-- (find-idrisgitfile "libs/base/Data/Vect.idr" "data Vect :")
isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat
mkSingle : (x : Bool) -> isSingleton x
mkSingle True = 0
mkSingle False = []
ssum : (single : Bool) -> isSingleton single -> Nat
ssum True x = x
ssum False [] = 0
ssum False (x :: xs) = x + ssum False xs
-- (find-idrisdoccpage (+ 1 11) "\"using\" notation")
-- (find-idrisdocctext (+ 1 11) "\"using\" notation")
data IsElem : a -> Vect n a -> Type where
Here : {x:a} -> {xs:Vect n a} -> IsElem x (x :: xs)
There : {x,y:a} -> {xs:Vect n a} -> IsElem x xs -> IsElem x (y :: xs)
{-
* (eepitch-to-buffer "*idris-repl*")
Vect 4 Nat
Vect
IsElem
:t IsElem
IsElem Nat
3 :: 4 :: Nil
[3, 4]
IsElem [3, 4]
-}
-- testVec : Vect 4 Int
-- testVec = 3 :: 4 :: 5 :: 6 :: Nil
-- inVect : IsElem 5 Main.testVec
-- inVect = There (There Here)
-- (find-idrisdoccpage (+ 1 12) "1.3.5 I/O")
-- (find-idrisdocctext (+ 1 12) "1.3.5 I/O")
-- (find-idrisdoccpage (+ 1 12) "1.3.6 \"do\" notation")
-- (find-idrisdocctext (+ 1 12) "1.3.6 \"do\" notation")
-- (find-idrisdoccpage (+ 1 13) "1.3.7 Laziness")
-- (find-idrisdocctext (+ 1 13) "1.3.7 Laziness")
-- (find-idrisdoccpage (+ 1 13) "1.3.8 Codata Types")
-- (find-idrisdocctext (+ 1 13) "1.3.8 Codata Types")
-- «useful-data-types» (to ".useful-data-types")
-- (find-idrisdoccpage (+ 1 14) "1.3.9 Useful Data Types")
-- (find-idrisdocctext (+ 1 14) "1.3.9 Useful Data Types")
-- (find-idrisdoccpage (+ 1 15) "List and Vect")
-- (find-idrisdocctext (+ 1 15) "List and Vect")
-- (find-idrisdocctext (+ 1 15) "List and Vect" "[1,2,3] means")
-- (find-idrisdoccpage (+ 1 15) " Aside: Anonymous functions and operator sections")
-- (find-idrisdocctext (+ 1 15) "Aside: Anonymous functions and operator sections")
-- (find-idrisdocctext (+ 1 15) "Aside: Anonymous functions and operator sections" "=>")
-- (find-idrisdoccpage (+ 1 17) "Dependent Pairs")
-- (find-idrisdocctext (+ 1 17) "Dependent Pairs")
-- (find-idrisdoccpage (+ 1 17) "vec : (n : Nat ** Vect n Int)")
-- (find-idrisdocctext (+ 1 17) "vec : (n : Nat ** Vect n Int)")
-- (find-idrisdoccpage (+ 1 17) "with (filter p xs)" "|")
-- (find-idrisdocctext (+ 1 17) "with (filter p xs)" "|")
-- (find-idrisdoccpage (+ 1 17) "Records")
-- (find-idrisdocctext (+ 1 17) "Records")
-- (find-idrisdoccpage (+ 1 19) "Dependent Records")
-- (find-idrisdocctext (+ 1 19) "Dependent Records")
-- «records» (to ".records")
-- (find-idrisdoccpage (+ 1 17) "Records")
-- (find-idrisdocctext (+ 1 17) "Records")
record Person where
constructor MkPerson
firstName, middleName, lastName : String
age : Int
fred : Person
fred = MkPerson "Fred" "Joe" "Bloggs" 30
{-
* (eepitch-to-buffer "*idris-repl*")
fred
firstName fred
age fred
:t firstName
record { firstName = "Jim" } fred
record { firstName = "Jim", age $= (+ 1) } fred
-}
-- (find-idrisgitfile "libs/prelude/Prelude.idr")
-- (find-idrisgitfile "libs/prelude/Prelude/List.idr")
-- (find-idrisgitfile "libs/base/Data/List.idr")
-- (find-idrisgitfile "libs/prelude/Prelude/")
-- (find-idrisgitfile "libs/prelude/Prelude/Bool.idr")
-- (find-idrisgitfile "libs/prelude/Prelude/Either.idr")
-- (find-idrisgitfile "libs/prelude/Builtins.idr" "data Pair :")
-- (find-idrisgitfile "libs/prelude/Builtins.idr" "data DPair :")
-- (find-idrisgitgrep "grep --color -nrH -e impossible libs/")
-- (find-idrisgitgrep "grep --color -nrH -e postulate libs/")
-- (find-idrisgitgrep "grep --color -nrH -e Vect libs/")
-- (find-idrisdoccpage (+ 1 179) "LinearTypes")
-- (find-idrisdocctext (+ 1 179) "LinearTypes")
-- «more-expressions» (to ".more-expressions")
-- (find-idrisdoccpage (+ 1 19) "1.3.10 More Expressions")
-- (find-idrisdocctext (+ 1 19) "1.3.10 More Expressions")
-- (find-idrisdoccpage (+ 1 19) "let bindings")
-- (find-idrisdocctext (+ 1 19) "let bindings")
-- (find-idrisdoccpage (+ 1 20) "List comprehensions" "[ expression | qualifiers ]")
-- (find-idrisdocctext (+ 1 20) "List comprehensions" "[ expression | qualifiers ]")
-- (find-idrisdoccpage (+ 1 20) "case expressions")
-- (find-idrisdocctext (+ 1 20) "case expressions")
-- (find-idrisdocctext (+ 1 20) "case expressions" "(== c)")
-- (find-idrisdoccpage (+ 1 21) "1.3.11 Totality")
-- (find-idrisdocctext (+ 1 21) "1.3.11 Totality")
-- «interfaces» (to ".interfaces")
-- (find-idrisdoccpage (+ 1 21) "1.4 Interfaces")
-- (find-idrisdocctext (+ 1 21) "1.4 Interfaces")
-- (find-idrisdoccpage (+ 1 22) "1.4.1 Default Definitions")
-- (find-idrisdocctext (+ 1 22) "1.4.1 Default Definitions")
-- (find-idrisdoccpage (+ 1 22) "1.4.2 Extending Interfaces")
-- (find-idrisdocctext (+ 1 22) "1.4.2 Extending Interfaces")
-- (find-idrisdoccpage (+ 1 23) "multiple constraints")
-- (find-idrisdocctext (+ 1 23) "multiple constraints")
-- (find-idrisdoccpage (+ 1 23) "1.4.3 Functors and Applicatives")
-- (find-idrisdocctext (+ 1 23) "1.4.3 Functors and Applicatives")
-- (find-idrisdoccpage (+ 1 23) "1.4.4 Monads and do-notation")
-- (find-idrisdocctext (+ 1 23) "1.4.4 Monads and do-notation")
-- (find-idrisdoccpage (+ 1 25) "do Just x_ok <- readNumber |")
-- (find-idrisdocctext (+ 1 25) "do Just x_ok <- readNumber |")
-- (find-idrisdoccpage (+ 1 25) "Monad comprehensions")
-- (find-idrisdocctext (+ 1 25) "Monad comprehensions")
-- (find-idrisdoccpage (+ 1 39) "filter p (x :: xs) |")
-- (find-idrisdocctext (+ 1 39) "filter p (x :: xs) |")
-- (find-idrisdoccpage (+ 1 39) "with clause, followed by a vertical bar |")
-- (find-idrisdocctext (+ 1 39) "with clause, followed by a vertical bar |")
-- (find-idrisdoccpage (+ 1 173) "Records")
-- (find-idrisdocctext (+ 1 173) "Records")
-- «theorem-proving» (to ".theorem-proving")
-- (find-idrisdoccpage (+ 1 40) "1.9 Theorem Proving")
-- (find-idrisdocctext (+ 1 40) "1.9 Theorem Proving")
-- (find-idrisdoccpage (+ 1 40) "1.9.1 Equality")
-- (find-idrisdocctext (+ 1 40) "1.9.1 Equality")
-- (find-idrisdoccpage (+ 1 41) "1.9.2 The Empty Type")
-- (find-idrisdocctext (+ 1 41) "1.9.2 The Empty Type")
-- (find-idrisdoccpage (+ 1 41) "1.9.3 Simple Theorems")
-- (find-idrisdocctext (+ 1 41) "1.9.3 Simple Theorems")
-- plusReduces : (n:Nat) -> plus Z n = n
-- plusReducesZ : (n:Nat) -> n = plus n Z
-- plusReducesZ Z = Refl
-- plusReducesZ (S k) = cong (plusReducesZ k)
-- cong : {f : t -> u} -> a = b -> f a = f b
-- plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
-- plusReducesS Z m = Refl
-- plusReducesS (S k) m = cong (plusReducesS k m)
{-
* (eepitch-to-buffer "*idris-repl*")
plusReducesZ 3
plusReducesS 3 4
3 = 3
3 = 4
Refl
Refl 3
Refl Nat
impossible
-}
-- (find-idrisdoccpage (+ 1 42) "1.9.4 Theorems in Practice")
-- (find-idrisdocctext (+ 1 42) "1.9.4 Theorems in Practice")
-- parity : (n:Nat) -> Parity n
-- parity Z = Even {n=Z}
-- parity (S Z) = Odd {n=Z}
-- parity (S (S k)) with (parity k)
-- parity (S (S (j + j))) | Even = Even {n=S j}
-- parity (S (S (S (j + j)))) | Odd = Odd {n=S j}
-- Unfortunately, this fails with a type error:
--
-- When checking right hand side of with block in views.parity with expected type
-- Parity (S (S (j + j)))
--
-- Type mismatch between
-- Parity (S j + S j) (Type of Even)
-- and
-- Parity (S (S (plus j j))) (Expected type)
-- (find-idrisdoccpage (+ 1 45) "1.10 Provisional Definitions")
-- (find-idrisdocctext (+ 1 45) "1.10 Provisional Definitions")
-- (find-idrisdoccpage (+ 1 48) "1.10.2 Suspension of Disbelief")
-- (find-idrisdocctext (+ 1 48) "1.10.2 Suspension of Disbelief")
-- (find-idrisdoccpage (+ 1 55) "1.13.1 Implicit arguments")
-- (find-idrisdocctext (+ 1 55) "1.13.1 Implicit arguments")
-- (find-books "__logic/__logic.el" "hindley-seldin2")
-- (find-hindleyseldin2page (+ 14 61) "4D Abstract numerals and Z")
-- (find-idrisdoccpage (+ 1 135) "5.2 Curry-Howard correspondence")
-- (find-idrisdocctext (+ 1 135) "5.2 Curry-Howard correspondence")
-- (find-idrisdoccpage (+ 1 135) "the (1=1) Refl")
-- (find-idrisdocctext (+ 1 135) "the (1=1) Refl")
-- (find-idrisdoccpage (+ 1 136) "5.2.1 And (conjunction)")
-- (find-idrisdocctext (+ 1 136) "5.2.1 And (conjunction)")
-- (find-idrisdoccpage (+ 1 136) "5.2.2 Or (disjunction)")
-- (find-idrisdocctext (+ 1 136) "5.2.2 Or (disjunction)")
-- (find-idrisdoccpage (+ 1 137) "``postulate``")
-- (find-idrisdocctext (+ 1 137) "``postulate``")
{-
* (eepitch-to-buffer "*idris-repl*")
2 = 2
3 = 4
Refl -- err
:t Refl
the (2 = 2)
the (2 = 2) Refl
the (3 = 4)
the (3 = 4) Refl -- err
Pair
Pair Nat Nat
Either Nat Int
Int
Bool
-}
-- (find-fline "~/IDRIS/Yoneda.idr")
-- (find-idrisgitfile "libs/prelude/Builtins.idr" "data Pair :")
-- proo : (P, Q, R : Type) -> Type
-- proo : (p, q, r : Type) -> Type
proo : Type -> Type -> Type -> Type
proo p q r = (Pair p q) -> r
-- proo = ?proo
-- proo p q r = Nat
-- (find-idrisdoccpage (+ 1 179) "| Impossible")
-- (find-idrisdocctext (+ 1 179) "| Impossible")
{-
* (eepitch-to-buffer "*idris-repl*")
proo
Nat
AndIntro
the Integer -3
the Nat -3
MkPair
-}
-- «Pair» (to ".Pair")
-- (find-es "idris" "idris2-mode")
--
-- Local Variables:
-- coding: utf-8-unix
-- modes: (idris2-mode idris-mode)
-- End: