Jon Sterling
Jon Sterling
There seems to be a much more fundamental problem with this definition beyond the bug in the typechecker: You've essentially defined equality of types `S,T` to be witnessed by a...
Seems to me that a much better solution would be to wait until we've got higher-kinded quantification and then just give leibniz equality...
I wonder if we can bring some attention to this PR again? I am having this problem and it would be great to have a fix merged.
Great idea!! This would be super useful IMO and it’s a beautiful bit of math. Sent from my iPhone > On Jul 8, 2021, at 4:37 PM, Alex Gryzlov ***@***.***>...
Might be good to see if we can get @robertharper to weigh in on this, particularly on the question of whether or not generative functors make sense in a Rust-like...
@zwarich Can you elaborate on how type abstraction can be used to enforce Haskell-style “coherence” in certain cases? This is interesting. @RobertHarper Hi Bob, Thanks for popping in. I was...
Bob Re type classes and gen. functors, I think you are right, and I seem to recall that we had a similar conversation at one point where I raised a...
Bob, do you have a paper or any literature that summarizes your re-working of data types? If I recall correctly, the idea was to support something like this: ``` sml...