Home

IdrisTddNotes

Notes from reading Type Driven Development with Idris.
This Wiki contains test and example programs compiled to markdown.

There is a small portion of Java developers who dream about programming in Scala.
There is a sizable portion of Scala developers who dream about programming in Haskell.
All Haskell programmers want to program in Idris.
;)

WORK IN PROGRESS

These notes compare Idris code in the book against Haskell. My goal is to write Haskell code very closely mimicking Idris to see value added by dependent types.

This comparison is somewhat unfair to Haskell as I am converting examples from a book about Idris and I try to keep Haskell code as close to Idris as possible. Idris is playing on its own turf so to speak.

The other reason for the unfairness is a risky assumption that I know how Haskell :). Or know enough of it to make the comparison meaningful.

TOC

Part 1

• idrVsHs_Part1_Sec1_4_5 - StringOrInt : Bool -> Type example
• idrVsHs_Part1_Sec2_2_2 - the function vs Haskell vs Groovy

Part 2

• idrVsHs_Part2_Sec3_2_3 - code generation/synthesis for Vect map
• idrVsHs_Part2_Sec4_2_2 - code generation/synthesis for Vect zip and append
• idrVsHs_Part2_Sec5_3_3 - dependent pair as VectorUnknown in Haskell
• idrVsHs_Part2_Sec6_1_1 - type level functions vs type synonyms and type families in Haskell
• idrVsHs_Part2_Sec6_2_1 - multi-parameter adder example
  • _I had to realign Nat from GHC.TypeLits using (n - 1) predecessor logic instead of (1 + n) or (n + 1) for things to work.
  • type family solution did not work with GHC.TypeLits Nat but worked with redefined Nat (not literal)
  • I am slowly abandoning GHC.TypeLits /src/Util/NonLitsNatAndVector
• idrVsHs_Part2_Sec6_2_2 - typesafe printf
• idrVsHs_Part2_Sec6_3 - data store with changing schema example, monadic parsers /src/Util/MiniParser.idr. singletons version is very similar /src/Part2/Sec6_3sing.hs.
• idrVsHs_Part2_Sec8_1 - simple equality proofs
• I failed to do meaningful job converting reverse Vector example form Section 8.2
• idrVsHs_Part2_Sec8_2_5 - + theorems and vector append with reversed signature
• idrVsHs_Part2_Sec8_2z - vector reverse example

`singletons` are used (more and more) from here on

• idrVsHs_Part2_Sec8_3 - Dec/DecEq using Nat and MyPair, exactLength example
• idrVsHs_Part2_Sec9_1 - type safe elem functions
• idrVsHs_Part2_Sec9_2 - hangman game
• idrVsHs_Part2_Secz10_1 - ListLast, SplitList view, reverse, mergeSort, TakeN examples

Idris goodness

(TODO)

• _ == "Idris, You figure it out"
  • Sec5_3_3.idr
• code generation
  • Sec3_2_3.idr
  • Sec4_2_2.idr
• dependent pairs
  • Sec5_3_3.idr
• pattern match informed by views

Some interesting links

https://personal.cis.strath.ac.uk/conor.mcbride/pub/hasochism.pdf
https://blog.jle.im/entry/introduction-to-singletons-1.html
https://blog.jle.im/entry/introduction-to-singletons-2.html
https://typesandkinds.wordpress.com/2012/12/01/decidable-propositional-equality-in-haskell/

Environment

Currently using ghc 8.2.2 and Idris 1.2.0

FYI about stack/ghc To play with newer version of TypeLits and singletons I have upped ghc/stack to lts-11.5 / 8.2.2. This is known to be a problem for older version of stack. If your stack come with ghc distribution, stack update may not work. I had to delete stack symbolic link in /usr/local/bin and reinstall it.

Idris instructions

• To compile run make from root directory
• To run repl navigate to src directory first and start repl there (idris repl)