Syntax of refinement types

[jllang]

I've read through the chapters 1 to 7 and haven't come accross a definition of the syntax of refinement types. I was expecting to see it rather early in the book. A BNF would be helpful. It seems that sometimes the same condition needs to be formulated differently in Haskell and LiquidHaskell. Mixing up Haskell and LiquidHaskell syntax seems to lead into often quite cryptic errors.

[ranjitjhala]

This is a great suggestion. I’ve added it elsewhere (in talks/slides) but would really help here too! Are there particularly tricky/egregious mismatches that you recall?

On Tue, Jul 13, 2021 at 5:37 AM John Lång @.***> wrote:

I've read through the chapters 1 to 7 and haven't come accross a definition of the syntax of refinement types. I was expecting to see it rather early in the book. A BNF would be helpful. It seems that sometimes the same condition needs to be formulated differently in Haskell and LiquidHaskell. Mixing up Haskell and LiquidHaskell syntax seems to lead into often quite cryptic errors.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquidhaskell-2Dtutorial_issues_110&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=S16HXtwImXn3-oN6dOvMcFXdHw8FwAIqdU3g0lQ5Iw0&s=Tcc3I6Rzj27YWP6W9oxs7NGr3SiQyqsinrqjOuyM89o&e=, or unsubscribe https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OFROIXQAM6JSAL2VVLTXQXPTANCNFSM5AJAQUHA&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=S16HXtwImXn3-oN6dOvMcFXdHw8FwAIqdU3g0lQ5Iw0&s=Cjnp5PyihmO_HtLz4D3e8_0q81KP5SSZGB4x1lCko4c&e= .

[jllang]

Apparently, things like lambda terms and infix notation with backticks don't work with refinement types. This example is quite contrived but I think it makes my point clear: The type of lists of odd integers can be expressed as follows: {-@ type ListOdd = {xs : [Int] | filter odd xs == xs} @-} As filter takes two arguments, the expression filter odd xs == xs should be the same as odd `filter` xs == xs but if I try to write {-@ type ListOdd = {xs : [Int] | odd `filter` xs == xs} @-} I get the error saying

~/liquidhaskell-tutorial/src/Tutorial_08_Measure_Set.lhs:658:24: error:
    • Cannot parse specification:
    unexpected ":"
    expecting operator, white space or "}"
    • 
    |
658 | {-@ type ListOdd = {xs : [Int] | odd `filter` xs == xs} @-}
    |                        ^

The error message makes it look like as if the problem was with the colon while in reality the cause was the use of backticks. Of course, using filter as an infix function like this would be weird, but I think you get my point.

[jllang]

I think that a chapter listing some common error types along with explanations would be very valuable to beginners like me.

[jllang]

I take it that the backticks are not supported by the refinement type syntax. A beginner might be tempted to try to use them.