New abstract refinements syntax

[spinda]

@ranjitjhala, @gridaphobe, @nikivazou, @christetreault, and I discussed this last week. I believe I remember the new syntax but don't want to risk getting it wrong—does anyone want to write it down here?

[nikivazou]

@spinda, we said that we will totally change the syntax (and the meaning) of Abstract Refinements, Thus we could defer this edit in the future. Does it block you right now?

[spinda]

@nikivazou, no, I'm just creating this so we can track it when it happens eventually and/or get ideas in writing.

[ranjitjhala]

For the record, is a link to the new syntax proposal

https://github.com/ucsd-progsys/liquidhaskell/blob/develop/Syntax.md#new-proposal

[yanhasu]

Whilst we're changing the syntax, why not de-tuple the abstract refinements? e.g. writing type BST a = BinaryTree a <\root -> LessThan root> <\root -> GreaterThan root> seems slightly more Haskell-y than type BST a = BinaryTree a <{\root -> LessThan root}, {\root -> GreaterThan root}> which is what we've currently got.

[nikivazou]

@yanhasu are you actively changing the syntax?

[yanhasu]

@nikivazou I haven't written anything yet, but I'm willing to have a go at implementing this.

[yanhasu]

@ranjitjhala some other points about the new proposal:

• The curly braces { } are already highly overloaded (HS records, HS layout, LH refinements, LH refinements of (), ...).
  • Perhaps a new keyword (refining, SubtypeOf,...) would be more self-documenting?
  • We can cook up ambiguity, e.g. the string {foo bar} could be...
    • ... a proof type (foo :: a -> Bool,bar :: a for some type a :: *)
    • ... a refinement kind (foo :: * -> *, bar :: * type variables)
• Does the 'type with shape' syntax really make all explicit applications redundant? How about:
  • type BST a = Tree a <\x -> {y:a | y<x },\x -> {y:a | x<y }>?
  • mergeSort :: (Ord a) => List a -> List a <\x -> {y:a | x<=y }>?
• What are the details of the 'meet' operator /\?
  • Can it intersect any two types?
    • Int /\ Bool?
    • Int /\ (a -> a)?
    • (a -> b) /\ (c -> d)?
    • (forall a. T1) /\ T2?
  • Does it behave just like the old point-free refinement syntax (e.g. Int<isEven>)?
    • If the intention is just to disambiguate syntax, why not just scrap point-free refinement? (so we'd use {v:Int | isEven v} instead)
• How do we use 'type-with-shape'-style abstract refinements inside normal (comprehension-style) refinements?
  • Currently, we can use papp1 to treat abstract refinements like normal measures to Bool.
  • How do we adapt this to the new syntax?
    • If we keep papp1, it becomes a hasType predicate, which sounds expressive (maybe too expressive?)
    • If we drop papp1, abstract refinements become a bit less expressive.