type level strings

[mutjida]

Is it possible for liquid haskell to get the values of type level literals? For example if I have a data type:

data T (x :: Symbol) a = T [a]

Can liquid haskell make use of the String which corresponds to the parameter on T?

e.g.

{-@ 

data T x a = T {v : [a] | len v == len x}

@-}

thanks,

  Jeff

[Niki Vazou]

The short answer is no. Types cannot appear in the refinements.

But you can fake it, by adding an extra value parameter that is aways equal to the string x.

I am interested to see your whole example of you are willing to share it.

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 liquidhaskel...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Ranjit Jhala]

​To elaborate, currently LH doesn't let you refer to "types" inside "refinements" -- (you can only refer to "values" inside refinements).

We'd be curious what your use case is, though since we 

are thinking about removing this restriction.

That said, you can do the following:

  data T a = T { x     :: String 

               , value :: {v: [a] | len v == len x }

               }

i.e. simply encode your invariants directly with values.

Would this work for you?

[Ranjit Jhala]

(And then of course, you'd use the usual "value" level strings directly...)

[jeff p]

Adding the value back into the data type would certainly allow me to write the constraints I need, but it would be a bit of a capitulation as there is no need for the value and all the necessary info is in the type. I think users will want to use values of type level literals in their constraints. In general, there are situations where you want to compute something and stick into the type some information about how the computation was done (e.g. a seed value); then you might want to prove invariants of the construction, with liquid haskell, which rely on that information. I think for the sake of proving correctness I will just make a version with the unnecessary argument and then wave my hands a little about the real implementation also being correct.

I was also wondering if it would be possible to use abstract refinements to do what I am after, i.e. create an abstract refinement when the value is around and then pass it to the datatype with the type level value. My experiments with this have not been encouraging-- I think I've run into a mixture of my own syntactic mistakes and possibly some liquid haskell bugs-- but I'd like to know if you think it's possible before I start asking concrete questions.

thanks,

  Jeff

[Niki Vazou]

Hey Jeff, I get the following error when I tried your code 

resources/custom/liquidhaskell/sandbox/1458413579_6077.hs:5:1: Error: GHC Error parse error (possibly incorrect indentation or mismatched brackets)

It is definitely possible to combine Abstract and Bounded Refinements to model what you have in mind, but it will indeed require some (a lot of) effort. 

I am positive, because I believe (without any formal proof yet) that you can use Bounded Refinement Types to encode _any_ ghost variable. As an example see this code:

{-@ T :: forall <p :: x:Symbol -> [a] -> Prop, q :: s:Symbol -> x -> Prop>. 

               {x::Symbol |- ([a])<p> <: {v:[a] | len v == len x}}

               {x::Symbol |- x<q> <: {v:x | v == x}}

               ([a])<p> -> T x a @-}

You can refine the data constructor `T` using two abstract refinements `p` on lists and `q` on the type variable `x` , so that 

- bound 1: p implies your desired length constraint

- bound 2: q relates somehow the symbol x and the type variable x 

So, in theory you can use AR to encode what you want. In practice

  

- We have never tried this kind of encoding before, so you will most probably hit many LH bugs. 

- I do not know how proofs on `T` will work, as to use `T` the specification requires the existence of a Symbol `x` that will not exist in your code. 

- Note that I am just refining the type constructor `T` because currently the refined data definition does not support any bounds. 

Will be happy to help of you have more concrete questions! 

Good luck:)

Niki

Niki Vazou

[jeff p]

I had meant the previous code I posted to be pseudo-code; sorry if that wasn't clear.

Thanks for the paper pointer. Is the construct and syntax you used documented somewhere? I'm not very confident that I understand what you're doing.

I am currently concentrating on a version with an explicit term level value, but I'd be interesting in picking this approach up again if it looks promising.

thanks,

  Jeff

[Ranjit Jhala]

The term-level value version is likely to be much more robust IMO :)

[Niki Vazou]

Definitely the term-level version will be easier to encode. 

Using bounds, we use the curly braces {x:t, ...., x:t |- t1 <: t2} to constraint or bound t1 to be a subtype of t2. Usually wither t1 or t2 contain abstract refinements(AR). This way, instead of defining a type signature that holds for all abstract refinements we define a signature that only holds for AR satisfying the bounds. 

You can read these signatures as 

abstract refinements <-> haskell type variables

bounds <-> bounds 

I believe that this approach is feasible, but it would require more effort from your and our side as we have never used bounds like this before. So, feel free to contact me for further details if you want to pursuit this approach