## New Syntax for Abstract Refinements

### Ghost Parameters


```haskell
A n -> B (n + 1)

-- becomes
{ p n => q (n + 1)}. A<p> -> B<q>

-- i.e.
{ p n => v = n + 1 => q v}. A<p> -> B<q>
```

which means, I suppose that

```haskell
A n -> B (op n)

-- becomes
{ p n => q (op n) }. A<p> -> B<q>

-- i.e.

{ p n => v = op n => q v }. A<p> -> B<q>
```


(a -> Count b <<p>>) -> xs:List a -> (Count (List b) <<q>>)


```haskell
A n -> B m -> C (n + m)

-- becomes
{ p n => q m => r (n + m) }. A<p> -> B<q> -> C<r>

-- i.e.
{ p n => q m => v = n + m => r v }. A<p> -> B<q> -> C<r>
```

{ n::Int<p> |- {v:Int | v = n+1} <: Int<q> }

```haskell
{-@ bump1 :: forall <p::Int -> Bool, q::Int -> Bool>.
               { n::Int<p> |- {v:Int | v = n + 1} <: Int<q> }
               (Int -> Int<p>) -> Int<q>
  @-}
bump1 :: (Int -> Int) -> Int
bump1 f = f 0 + 1

{-@ bumps :: forall <p::[Int] -> Bool, q::Int -> Bool>.
               { xs :: [Int]<p> |- {v:Int | v = len xs} <: Int<q> }
               (Int -> [Int]<p>) -> Int<q>
  @-}

bumps :: (Int -> ListN Int n) -> IntN n
bumps f = size (f 0)

{-@ bump2 :: forall <p::Int -> Bool, q::Int -> Bool, r::Int -> Bool>.
               { n::Int<p>, m::Int<q> |- {v:Int | v = n + m} <: Int<r> }
               (Int -> Int<p>) -> (Int -> Int<q>) -> Int<r>
  @-}
bump2 :: (Int -> Int) -> (Int -> Int) -> Int
bump2 f g = f 0 + g 0

{-@ flerb :: ({v:Int | v = 6}, {v:Int | v = 10}) @-}
flerb = (a, b)   
  where
    a = bump  zong
    b = bump2 zong zong
    zong :: Int -> Int
    zong n = 5

{-@ type IntN N = {v:Int | v == N} @-}
bump1 :: Ghost n. (Int -> IntN n) -> IntN (n+1)
bump2 :: Ghost n m. (Int -> IntN n) -> (Int -> IntN m) -> IntN (n+m)
```

### New Proposal

**NOTE:** I believe this is a **purely syntactic change**:
it should not affect how absref is actually implemented,
but it more precisely describes the implementation than
the current `-> Bool` formulation.

#### Step 1: Abstract Refinement is "Type with Shape"

Key idea is to think of an abstract refinement as a (function returning a) refinement type.

That is, the abstract refinement:

```haskell
  T1 -> T2 -> T3 -> ... -> S -> Bool
```

now just becomes

```haskell
  T1 -> T2 -> T3 -> ... -> {S}
```

Here, `{S}` denotes a refinement type with shape `S`

**Key Payoff:** This means that we don't need an _explicit application_ form, that is

```haskell
  foo :: forall <p :: Int -> Bool>. [Int<p>] -> Int<p>
```

can just be written as

```haskell
  foo :: forall <p :: {Int}>. [p] -> p
```

where we need not write `Int<p>`, its enough to just write `p`.

#### Step 2: An explicit "Meet" Operator

However, sometimes you need to write things like:

```haskell
  List <p> a <<p>>
```

where `p :: List a -> Bool` i.e. `p :: {List a}` and which denotes

* a list-of-a that is recursively indexed by `p`, AND
* where the top-level list is constrained by `p`.

That is, more generally, where you want to

* additionally, index the type with other abstract refinements, AND
* "apply" an abstract refinement to the "top-level" type.

For this, I think we should have an explicit *meet* operator
Note that, earlier `Int<p>` was an *implicit* meet operator,
where we were *conjoining* `Int` and `p`. Viewing `p` as
just being a refined `Int` allows us to SEPARATE "meet"
to only those places where its really needed.

So we can write the funny `List <p> a <<p>>` as:

```haskell
  p /\ List <p> a
```

See below for many other examples:

#### Example: Value Dependencies

**Old**

```haskell
  foo :: forall <p :: Int -> Int -> Bool>. x:Int -> [Int<p x>] -> Int<p x>
```

**New**

```haskell
  foo :: forall <p :: Int -> {Int}>. x:Int -> [p x] -> p x
```

#### Example: Dependent Pairs

**Old**

```haskell
  data Pair a b <p :: a -> b -> Bool>
    = Pair { pairX :: a
           , pairB :: b<p pairX>
           }

  type OrdPair a = Pair <{\px py -> px < py}> a a
```

**New**

```haskell
  data Pair a b <p :: a -> {b}>
    = Pair { pairX :: a
           , pairY :: p pairX
           }


  type OrdPair a = Pair a a <\px ->  {py:a | px < py}>
```

#### Example: Binary Search Maps

**Old**

```haskell
  data Map k a <l :: root:k -> k -> Bool, r :: root:k -> k -> Bool>
      = Tip
      | Bin { mSz    :: Size
            , mKey   :: k
            , mValue :: a
            , mLeft  :: Map <l, r> (k <l mKey>) a
            , mRight :: Map <l, r> (k <r mKey>) a }

  type OMap k a = Map <{\root v -> v < root }, {\root v -> v > root}> k a
```

**New**

```haskell
  data Map k a <l :: root:k -> {k}, r :: root:k -> {k}>
      = Tip
      | Bin { mSz    :: Size
            , mKey   :: k
            , mValue :: a
            , mLeft  :: Map (l mKey) a <l, r>
            , mRight :: Map (r mKey) a <l, r> }

  type OMap k a = Map k a <\root -> {v:k | v < root }, \root -> {v:k | root < v}>
```

#### Example: Ordered Lists

**Old**

```haskell
  data List a <p :: a -> a -> Bool>
    = Emp
    | Cons { lHd :: a
           , lTl :: List <p> (a<p lHd>)
           }

  type OList a = List <{\x v -> x <= v}> a
```

**New**

```haskell
  data List a <p :: a -> {a}>
    = Emp
    | Cons { lHd :: a
           , lTl :: List (p lHd) <p>
           }

  type OList a = List a <\x -> {v:a | x <= v}>
```

#### Example: Infinite Streams

**Old**

```haskell
  data List a <p :: List a -> Prop>
    = N
    | C { x  :: a
        , xs :: List <p> a <<p>>
        }

  type Stream a = {xs: List <{\v -> isCons v}> a | isCons xs}
```

**New**

```haskell
  data List a <p :: {List a}>
    = N
    | C { x  :: a
        , xs :: p /\ List a <p>
        }

  type Stream a = {xs: List a <{v | isCons v}> | isCons xs}
```




### Old Proposal


|                      | Current Syntax                | Future Syntax                 |
|----------------------|-------------------------------|-------------------------------|
| Abstract Refinements | `List <{\x v -> v >= x}> Int` | `List Int (\x v -> v >= x)`   |
|                      | `[a<p>]<{\x v -> v >= x}>`    | `[a p] (\x v -> v >= x) (??)` |
|                      | `Int<p>`                      | `Int p`                       |
|                      | `Int<\x -> x >=0>`            | `Int (\x -> x >= 0)`          |

|                      | `Maybe <<p>> (a<q>) (?)`      | `Maybe (a q) p`               |
|                      | `Map <l, r> <<p>> k v  (?)`   | `Maybe k v l r p`             |

| Type Arguments       | `ListN a {len xs + len ys}`   | `ListN a (len xs + len ys)`   |

Q: How do I distinguish `Int p` with `ListN a n`?
(`p` is a abstract refinement and `n` is an `Integer`)

A: From the context!
Use simple kinds, i.e.
`ListN :: * -> Int -> *`
`Int :: ?AR -> *`