Equality constraints (~): type-theory behind them

[Brandon Allbery]

I think the point is more that runtime evidence means passing an additional
type witness around, potentially changing generated code and even behavior
(if this causes dictionary passing where none had been needed previously).
It's not addressing your question.

On Sat, Dec 22, 2018 at 11:48 PM Anthony Clayden <
anthony_clayden at clear.net.nz> wrote:

>
>
> On Sat, 22 Dec 2018 at 7:08 PM, Anthony Clayden <
> anthony_clayden at clear.net.nz> wrote:
>
>>
>> On Mon, 10 Dec 2018 at 6:12 PM, Anthony Clayden <
>> anthony_clayden at clear.net.nz> wrote:
>>
>>> On Mon, 10 Dec 2018 at 9:36 PM, Tom Schrijvers wrote:
>>>
>>>> Maybe our Haskell'17 paper about Elaboration on Functional Dependencies
>>>> sheds some more light on your problem:
>>>>
>>>> https://people.cs.kuleuven.be/~tom.schrijvers/Research/papers/haskell2017a.pdf
>>>>
>>>>
>>>
>> I feel I'm not getting much light shed. No amount of adding `(~)` in GHC
>> nor `TypeCast`+`typeCast` method in Hugs will get #9627 function `f` to
>> compile. So my 'specific example' earlier in this thread shows `(~)` is
>> moderately eager/more eager than FunDeps alone, but not eager enough for
>> #9627.
>>
>
>
> Can anybody explain @yav's comment here
>
> https://github.com/ghc-proposals/ghc-proposals/pull/158#issuecomment-449590613
> "currently equality constraints have no run-time evidence associated with
> them".
>
> Haskell has type-erasure semantics. Why would I need any _run-time_
> evidence for anything to do with type improvement? What impact would the
> lack of evidence have at run-time?
>
> Does this mean `(~)` constraints don't produce evidence at compile time?
> Which is also the difficulty for type improvement under FunDeps.
>
> (I tried a type family to achieve the same effect as `(~)` with an
> injective TF. No improvement in improvement.)
>
>
> AntC
>
>>
>
>> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>


-- 
brandon s allbery kf8nh
allbery.b at gmail.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20181222/f21081b2/attachment.html>