Type equalities

[nikivazou]

Type equalities are treated as class constraints (as of recently). So the following test passes

{-# LANGUAGE TypeFamilies   #-}

{-@ zoo :: x:a -> y:a -> {v:b | v ~~ x} @-}
zoo :: (a~b) => a -> a -> b 
zoo x _ = x 

Next step is to push the equality information in the logic and allow replacing v~~x with v == x. The second is not malformed.

[gridaphobe]

Is there a reason to push the type equality into the logic? (Besides the ugliness of ~~?)

[nikivazou]

Yes! I want to also have < etc, not only ~~

[ranjitjhala]

Can you think of a way to NOT push type equality into the logic? I don't think that's a good idea.

On Tuesday, May 3, 2016, Eric Seidel notifications@github.com wrote:

Is there a reason to push the type equality into the logic? (Besides the ugliness of ~~?)

— You are receiving this because you are subscribed to this thread. Reply to this email directly or view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/701#issuecomment-216657729

[nikivazou]

I think we need to reason about all the type class info properly: right now we have a hack for numerics, we should generalize it with a better story

[ranjitjhala]

Not seeing the connection of type classes and equality constraints ...

On Tuesday, May 3, 2016, Niki Vazou notifications@github.com wrote:

I think we need to reason about all the type class info properly: right now we have a hack for numerics, we should generalize it with a better story

— You are receiving this because you commented. Reply to this email directly or view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/701#issuecomment-216659739

[nikivazou]

They are very similar

• arguments are inferred by the compiler
• they are printed before => in the type signature
• both are represented as type constructors applied to types

Actually, I expected ~ to be a class constraint, but it is not

[gridaphobe]

Yes, class constraints are very different from equality constraints. (< would count as a class constraint)

[gridaphobe]

Specifically, the fancier constraints, like the arithmetic operators could be useful to push into the logic, but the equality constraints seem pointless to me.

[nikivazou]

@gridaphobe I want to be able to write

{-# LANGUAGE TypeFamilies   #-}

{-@ zoo :: (a~b) => x:a -> y:a -> {v:b | v < x} @-}
zoo :: (a~b) => a -> a -> b 
zoo x _ = x

[ranjitjhala]

@nikivazou, why do you want to write that? Whats wrong with:

{-@ zoo :: x:a -> y:a -> {v:b | v < x} @-}
zoo :: (a~b) => a -> a -> b
zoo x _ = x

or at any rate, for LH emitting FQ constraints that would be

equivalent to what we get from the above?

On Tue, May 3, 2016 at 2:08 PM, Niki Vazou notifications@github.com wrote:

@gridaphobe https://github.com/gridaphobe I want to be able to write

{-# LANGUAGE TypeFamilies #-}

{-@ zoo :: x:a -> y:a -> {v:b | v < x} @-} zoo :: (a~b) => a -> a -> b zoo x _ = x

— You are receiving this because you commented. Reply to this email directly or view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/701#issuecomment-216665053

[nikivazou]

@ranjitjhala under an environment that does not know a~b, the refinement you wrote is unsorted, as it reduces to x:a, v:b |- v < x

[gridaphobe]

1. Why do you want to write that? In my experience writing an explicit equality constraint in the context is a bad sign.
2. Why not just apply the equality before running the sort-checker?

[nikivazou]

I did not understand your 2 point.

The reason I want to do that is here https://github.com/ucsd-progsys/liquidhaskell/pull/700/commits/44637d5eb2b961979012e9c0c78b3bb4aab07a7b

but I can see more Haskell users asking this feature.

[gridaphobe]

You can treat the equality as a substitution a := b, to be applied before sort-checking. Then there's no need to deal with equality constraints in the logic.

[nikivazou]

That is a nice solution!

[ranjitjhala]

@nikivazou -- sorry I cut paste without editing, I meant just replace all a with b or vice versa...

On Tue, May 3, 2016 at 2:39 PM, Niki Vazou notifications@github.com wrote:

That is a nice solution!

— You are receiving this because you were mentioned. Reply to this email directly or view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/701#issuecomment-216673034

[ranjitjhala]

but to do that in LH not inside fixpoint.

On Tue, May 3, 2016 at 2:42 PM, Ranjit Jhala jhala@cs.ucsd.edu wrote:

@nikivazou -- sorry I cut paste without editing, I meant just replace all a with b or vice versa...

On Tue, May 3, 2016 at 2:39 PM, Niki Vazou notifications@github.com wrote:

That is a nice solution!

— You are receiving this because you were mentioned. Reply to this email directly or view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/701#issuecomment-216673034

[nikivazou]

So, more or less what Eric says. It is a solution!