Home

IdrisTddNotes

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.
;)

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

These notes compare Idris code in the book against Haskell. My goal is to write Haskell code very closely mimicking Idris to see the 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 reasons for the unfairness is a risky assumption that I know how to 'haskell' :), or that I know enough of it to make the comparison meaningful.

This work is mostly done, some cleanup work is still in progress
I also started working on Scala IdrisTddScalaNotes version of these notes in a separate project. This page links to equivalent code in in that project.

TOC

Part 1

• Part1_Sec1_4_5 - StringOrInt : Bool -> Type example. See also work-in-progress Sec1_4_5_StringOrIntAsGADT.scala.
• Part1_Sec2_2_2_the - the function vs Haskell vs Java/Groovy and Scala. See also work-in-progress Sec2_2_2_the.scala

Part 2

• Part2_Sec3_2_3_gen - code generation/synthesis for Vect map
• Part2_Sec4_2_2_gen - code generation/synthesis for Vect zip and append
• Part2_Sec5_3_3_dpair - dependent pair as VectorUnknown in Haskell
• Part2_Sec6_1_1_tyfunc - type level functions vs type synonyms and type families in Haskell
• Part2_Sec6_2_1_adder - multi-parameter adder example

I used `GHC.TypeLits` at the beginning but decided to abandon them from here on
(see [WorkingWithTypeLits.hs in my LC2019 presentation](https://github.com/rpeszek/present-proofs-lc19/blob/master/src/Present/WorkingWithTypeLits.hs))

• Part2_Sec6_2_2_printf - typesafe printf
• Part2_Sec6_3_datastore - data store with changing schema example, monadic parsers /src/Util/MiniParser.idr. singletons version is very similar /src/Part2/Sec6_3sing.hs.
• Part2_Sec8_1_eqproof - simple equality proofs
• Part2_Sec8_2_5_vappd - + Nat plus theorems and vector append with reversed signature
• Part2_Sec8_2z_reverse - vector reverse example

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

• Part2_Sec8_3_deceq - Dec/DecEq using Nat and MyPair, exactLength example

• Part2_Sec9_1_elem - type safe elem functions

• Part2_Sec9_2_hangman - hangman game

• Part2_Sez10_1_views - ListLast, SplitList, TakeN views, reverse, mergeSort, groupByN, and halves examples. This note also uses ``-XViewPatterns which is similar to Idris'with`. I am not using it elsewhere because it does not play well with `-fwarn-incomplete-patterns`.

• Part2_Sez10_2a_snoc - reverse using SnocList GADT - seems impossible to match linear cost of Idris code!

  • Part2.Sez10_2aVect.hs implements reverse Vect n a with SnocVect mimicking the type level code for list. I had to use :~~: instead of :~: as type equality. This is not a linear cost algorithm.
  • Part2.Sez10_2aVect2.hs implements a more straightforward SnocVect. No SVect, VAppend type families, etc are used. This version has linear cost if proofs cost is ignored as in ProofPerformance.

• Part2_Sez10_2b - isSuffix using SnocList GADT

  • Sez10_2e.idr (Exercises from 10.2) use advanced views and have linear cost. I can only see slower Haskell representations of these.

• Part2_Sez10_3_hiding - attempt to mimic ShapeView API

Part 3

• Sec14a_DoorJam - I have skipped converting 'Door' state machine example to Haskell.
• Part3_Sec14b_ATM - ATM protocol converted to Haskell. This program implements the very interesting and powerful monad-like DSL with safe state transitions. Unfortunately, I had to use unsafeCoerce converting the >>= to IO.
• Part3_Sec15a_ProcessLib - Dependently typed concurrent protocol library.
  • Concurrent programming is very error prone. I suffered quite a bit implementing version of Idris primitives here
• Part3_Sec15b_ProcessList - Example using the above library

Play

Set of notes and not book related experiments.

• Play_FunctorLaws - Functor Laws. Proofs for Maybe and List in Idris and Haskell
• Play_RankN - rank n types in Idris and Haskell
• Play_ProofPerformance - how to make proofs cost nothing

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
  • Part2_Sez10_1 and other in Sec10
• views result in faster performance
  • Part2_Sez10_2a

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 came 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)