<commit_before>## New Syntax for Abstract Refinements 

### 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.


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

That is, the abstract refinement:

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

now just becomes 

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

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

This means that we don't need an explict "application" form, that is

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

can just be written as

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

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


However, sometimes you need to write things like:

```
  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`.
<commit_msg>update Syntax.md with new abs-ref syntax proposal<commit_after>## New Syntax for Abstract Refinements 

### 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:

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

now just becomes 

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

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

This means that we don't need an explict "application" form, that is

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

can just be written as

```
  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:

```
  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`.

{'fraction_non_alphanumeric': 0.14855687606112053, 'fraction_numerical': 0.005942275042444821, 'mean_word_length': 3.2089285714285714, 'pattern_counts': {'":': 0, '<': 19, '<?xml version=': 0, '>': 47, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1000290', 'n_tokens_mistral': 811, 'n_tokens_neox': 750, 'n_words': 346}