[Haskell-cafe] Does the constraints library give (a :- b) -> Dict (a |- b)?
Tom Ellis
tom-lists-haskell-cafe-2023 at jaguarpaw.co.uk
Thu Nov 30 13:37:47 UTC 2023
The constraints library [1] has
implied :: forall a b. (a => b) => a :- b
from which I can obtain
implied' :: Dict (a |- b) -> a :- b
implied' Dict = implied
but can I get the converse of this, that is
coimplied :: (a :- b) -> Dict (a |- b)
coimplied = error "Can it be done?"
I don't see how. The library itself only mentions "|-" in its
definition. Would this combinator violate some guarantee that's
essential for the safe use of type classes?
I'm a bit confused why the same library allows abstraction over type
variables with forall_[2]
forall_ :: (forall a. Dict (p a)) -> Dict (Forall p)
but not abstraction over "term" variables (i.e. of kind Constraint),
as in coimplied.
Alternatively, can someone help me achieve my goal another way? That
is, I need to be able to dischange the quantified constraint
forall i. T0 i => T2 i
given that I can already discharge the constraint
forall i. T1 i => T2 i
and I have available the value
forall i. T0 i => Dict (T1 i)
>From the latter I can easily get
forall i. T0 i :- T1 i
But without coimplied I don't know how to proceed.
Thanks,
Tom
[1] https://hackage.haskell.org/package/constraints-0.14/docs/Data-Constraint-Forall.html
[2] https://hackage.haskell.org/package/constraints-0.14/docs/Data-Constraint-Forall.html#v:forall_
More information about the Haskell-Cafe
mailing list