tying the knot in LH

[Zilin Chen]

Hi,

Is there a way to give tying-the-knot style code a specification? E.g. f
I have datatype

```
data Expr a e
= Variable (Int, a)
| Fun FunName [Type] FunNote
| App (e a) (e a)
| ILit Integer
| Let a (e a) (e a)
```

and I'd like to write some predicates such as:

```
data Expr a e <t :: Int -> Prop, v :: Int -> Prop> = ...
```

I failed to find a way for the `(e a)' part, as `(e <t, v> a)` fails to
parse.

Thanks,
Zilin

[Niki Vazou]

Hello Zilin, 

We do not have a way to currently support your request, i.e. provide abstract refinements for type-variable data types. 

A problem that I see is that in `e <t, v> a` should be constrained so that it can only be instantiated with type constructors that accept the abstract refinements `t :: Int -> Prop` and `v :: Int -> Prop`. I cannot think of a clean solution for such checks.  

As a work around you can define your expression type recursively: 

http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1480270675_18382.hs

{-@

data Expr a <t :: Int -> Prop, v :: Int -> Prop>

  = Variable {evar :: (Int, a)}

  | App {eapp1 ::  Expr <t, v> a, eapp2 :: Expr <t, v> a}

  | ILit {elit :: Integer}

  | Let {elet1 :: a, elet2 :: Expr <t, v> a, elet3 :: Expr <t, v> a}

@-}

Out of curiosity, what is the meaning of `t` and `v`?

Best, 

Niki

--
You received this message because you are subscribed to the Google Groups "liquidhaskell" group.
To unsubscribe from this group and stop receiving emails from it, send an email to liquidhaskell+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Zilin Chen]

Thank you Niki.

In the Haskell version, we use `t` and `v` (both of kind (promoted) `Nat`) as in `data Expr a t v e = ...` to track the number of bound type/term variables. In general I see using predicates on datatypes be the best way to define indexed types in LH.

Cheers,
Zilin