search

ucsd-progsys / liquidhaskell

Liquid Types For Haskell
BSD 3-Clause "New" or "Revised" License
1.18k stars 134 forks source link

Wrappers for newtypes #841

Open nikivazou opened 7 years ago

nikivazou commented 7 years ago

If you defined a data type to wrap a value

data    Wrap a = Wrap {unwrap :: a }
{-@ data Wrap a = Wrap {unwrap :: a } @-}

Liquid Haskell will automatically turn unwrap into a measure.

Thus, just opening Wrap is enough (using the measure info) to prove the following equality

wrapTheorem :: Wrap a -> Proof 
{-@ wrapTheorem :: x:Wrap a -> {x == Wrap (unwrap x)} @-}
wrapTheorem (Wrap _) = trivial

If Wrap was a newtype, Wrap does not exist in core, instead, ghc is using casts to implement the above casting. The question is how can we prove theorem wrapTheorem if Wrap is defined to be a newtype, thus no measure definition is possible?

gridaphobe commented 7 years ago

We can rewrite the cast back to constructor application and case analysis, this is what I do for single-method classes.

nikivazou commented 7 years ago

We meaning a function we define in Liquid Haskell? Or can we just disable a simplification pass of ghc?

gridaphobe commented 7 years ago

I mean rewrite the Core from

foo `Cast` Foo ~ Wrap Foo

to

Wrap foo

and vice versa for unwrapping.

gridaphobe commented 7 years ago

Yes, LH would do this behind the scenes

nikivazou commented 7 years ago

Oh interesting idea! It should be though that a ghc transformation step does exactly the inverse! If we could deactivate it...

gridaphobe commented 7 years ago

Not necessarily, it may be baked into the desugaring step

gridaphobe commented 7 years ago

See

https://github.com/ucsd-progsys/liquidhaskell/blob/fc8c181c5d56f56851b50bb5be7d382f80698d02/src/Language/Haskell/Liquid/Constraint/Generate.hs#L995-L1028

for the code that already does this transformation for type classes.