How to simplify signatures?

[ivanperez-keera]

I'm writing some simple operations and I find myself with pretty long type constraints, such as:

( S.Nubable (S.Sort (x :++ S.Nub (S.Sort (y :++ '[]))))
, S.Nubable (S.Sort (y :++ '[]))
, S.Sortable (x :++ S.Nub (S.Sort (y :++ '[])))
, S.Sortable (y :++ '[])
)

I wonder if there's any way of shortening that to say that x and y are sortable and nullable, and let the compiler figure out that appending '[] and appending x to y also are. I tried the obvious way and that didn't work:

    • Could not deduce (Sortable (y :++ '[]))
        arising from a do statement
      from the context: (S.Nubable x, S.Nubable y, Sortable x,
                         Sortable y)

Also, in my function I am performing the union of x, y and the empty set, but I'd like the result to have type:

S.Union x y

instead of the longer:

S.Union x (S.Union y '[])

How to do this?

[ivanperez-keera]

Following up on my previous answer:

I see that there's this:

https://github.com/dorchard/type-level-sets/blob/master/src/Data/Type/Set.hs#L53-L56

No reference elsewhere in that module. My guess is that it could contain proofs of equality, that could then be used in type constraints. Assuming we can write those proofs in haskell, how could you use them in type constraints so that haskell accepts them and lets signatures be simpler?

[ivanperez-keera]

And a second question: let's assume that, temporarily, we are willing to accept some of those without proof (for instance, that the empty set is the identity for union). Given that we have undefined in haskell, is there a way to use that to our advantage to create any constraint we need, including those in the previous link, and say "believe me", or "this is an axiom"?

[jmorag]

There are some cases where you can use unsafeCoerce as a "trust me I know what I'm doing" escape hatch. See https://blog.josephmorag.com/posts/databass1/#headline-10 for an example.

[dorchard]

I have various thoughts about how to essentially embed proof equality terms that may help here. @ivanperez-keera do you have a MWE so we can experiment?