Typos

[ethanfrey]

I found the following minor issues when going through the web version of the tutorial:

Chapter 8, footnote 1, the link is broken. It should be: https://ucsd-progsys.github.io/liquidhaskell-blog/2013/03/26/talking-about-sets.lhs/

Chapter 8, the hint Hint: You may want to remind yourself about the dimension-aware signature for partition from the earlier chapter. needs to point to https://ucsd-progsys.github.io/liquidhaskell-tutorial/07-measure-int.html#/listreducing

The following example from chapter 8 is rejected with a rather unexpected warning (develop branch of liquidhaskell):

{-@ mergeSort :: (Ord a) => xs:List a -> ListEmp a @-}
mergeSort []  = []
mergeSort xs  = merge (mergeSort ys) (mergeSort zs)
  where
   (ys, zs)   = halve mid xs
   mid        = length xs `div` 2

**** RESULT: ERROR *************************************************************

 /Users/ethan/haskell/liquid/src/sets.hs:125:18: Error: Specified Type Does Not Refine Haskell Type for Sets.mergeSort

 125 | {-@ mergeSort :: (Ord a) => xs:List a -> ListEmp a @-}
                        ^

 The Liquid type

     forall t t. GHC.Classes.Ord t => [t] -> [t]

 is inconsistent with the Haskell type

     forall t t. GHC.Classes.Ord t => [t] -> [t]

 defined at /Users/ethan/haskell/liquid/src/sets.hs:126:1-9

But if I add an explicit Haskell type to this, it works:

{-@ mergeSort :: (Ord a) => xs:List a -> ListEmp a @-}
mergeSort :: (Ord a) => [a] -> [a]
mergeSort []  = []
mergeSort xs  = merge (mergeSort ys) (mergeSort zs)
  where
   (ys, zs)   = halve mid xs
   mid        = length xs `div` 2

I'm not sure if this is an error in liquid or a typo in the example

[ranjitjhala]

Thanks @ethanfrey, will fix those links!

The last one is a glitch in our pretty printer; it should say forall t1 t2 instead of forall t t but there is actually a subtle bug in your code that is being pointed out.

The error says that the Liquid type is different from the GHC inferred type (when you don't put in the type annotation.)

To see why, suppose this is the file (no type annotations.)

mergeSort []  = []
mergeSort xs  = merge (mergeSort ys) (mergeSort zs)
  where
   (ys, zs)   = halve mid xs
   mid        = length xs `div` 2

halve :: Int -> [a] -> ([a], [a])
halve = undefined

merge :: (Ord a) => [a] -> [a] -> [a]
merge = undefined 

Now when you fire it up in GHC

rjhala@borscht ~> ghci
GHCi, version 7.10.2: http://www.haskell.org/ghc/  :? for help
λ> :l tmp.hs 
[1 of 1] Compiling Main             ( tmp.hs, interpreted )
Ok, modules loaded: Main.
λ> :t mergeSort 
mergeSort :: Ord t1 => [t] -> [t1]

Aha. Notice that the input list of [t] yields an output list of [t1]... pretty odd. Can you spot the issue in the mergeSort code?

[ethanfrey]

Yeah, it never terminates....we split a list of one element, and it gives a [] and a list of one element, and then we split a list of one element....

Nice tip with ghci to check the sigs. I fixed the type signature to get liquid to run, then fixed the bug for the excercise. After your feedback, I realized that once the code was fixed, the type signature matched liquid as well.

I have to admit I am quite new to haskell and just going through the liquid haskell tutorial and find it a great introduction. Thank you all so much for this project.

[ranjitjhala]

Super! Thanks to you for the feedback!

On Sat, Apr 22, 2017 at 10:31 PM, Ethan Frey notifications@github.com wrote:

Yeah, it never terminates....we split a list of one element, and it gives a [] and a list of one element, and then we split a list of one element....

Nice tip with ghci to check the sigs. I fixed the type signature to get liquid to run, then fixed the bug for the excercise. After your feedback, I realized that once the code was fixed, the type signature matched liquid as well.

I have to admit I am quite new to haskell and just going through the liquid haskell tutorial and find it a great introduction. Thank you all so much for this project.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/48#issuecomment-296387048, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuODbN6ejdYbqRo6l_4v_q_9lmKIXhks5ryjJ8gaJpZM4NFC3Z .

[ranjitjhala]

Fixed by cfaae93