ucsd-progsys / liquidhaskell-tutorial

Tutorial for LiquidHaskell
https://ucsd-progsys.github.io/liquidhaskell-tutorial/
MIT License
75 stars 27 forks source link

Tim's issues #25

Open ranjitjhala opened 9 years ago

ranjitjhala commented 9 years ago
  1. the bizarre length --> len suggestion
  2. what is (!) in chapter 4
  3. chapter 4 is too sudden:
    • what is a measure exactly
    • rapid introduction of "accumulator" loops e.g. vector sum/ higher-order functions
    • specifically Inference: Our First Recursive Function (is complex because it uses an accumulator)
    • then the HOF examples are very complex (and should be explained later after EASY HOFs)
  4. solve 3 by writing a small "measures" chapter between 3 and 4 which has lists, len, average, simple recursive functions on lists etc. basically -- convert chapter 3 of lh-workshop into a simpler intermediate chapter with: (a) data types, (b) measures, (c) no recursion -- year, CSV (d) simple data-oriented recursion (e.g. map, append)
  5. The "measure" / Sec 2.6 bit in chapter 2 seems out of place, not really motivated well. Perhaps put into the 4 above and it would fit nicely.
  6. When you DO get into go style recursion with accumulators -- it is actually complex if the person has not seen it before, so more explanation there is helpful.
  7. Make clear what exactly is a DEFINITION (as in: enclose in a BOX explicitly marked as DEFINITION -- we are introducing a new keyword) e.g. "specification" (Ch 3 -- what IS a specification), or "verification" or "measures" (ch 4) or "assumes" -- when each such idea is introduced, mark it clearly as a new concept and give concrete examples.
  8. Perhaps reuse the "RefTypes = Types + Predicates" as the motif for introducing a new notion.
  9. For the more interesting examples -- have more discussion about
    • the right answer/ solution key
    • the other approaches
    • perhaps hidden behind a 'click here to discuss'
    • A nice example is the text around Exercise: (Vector Head) -- more of that would be valuable. +At the least, some solution to compare against.