Re: [was ghc-devs] Reasoning backwards with type families

2017-12-14 Thread Clinton Mead
Happy to go with the bogusness if it works better than injective types, feel free to submit a patch. :) On Thu, 14 Dec 2017 at 9:08 pm, Anthony Clayden < anthony_clay...@clear.net.nz> wrote: > On Thu, 14 Dec 2017 at 4:13 PM, Clinton Mead > wrote: > >> >> I've panicked

Re: [was ghc-devs] Reasoning backwards with type families

2017-12-14 Thread Anthony Clayden
On Thu, 14 Dec 2017 at 4:13 PM, Clinton Mead wrote: > > I've panicked GHC enough whilst developing Freelude so whilst I'm not sure > exactly what you're saying I'd be hestiant about exploiting anything bogus > (8.2 btw seems far more stable than 8.0 btw). > ;-) Fair

Re: [was ghc-devs] Reasoning backwards with type families

2017-12-13 Thread Anthony Clayden
On Thu, 14 Dec 2017 at 3:19 PM, David Feuer wrote: > I still haven't really digested what you've written, but I wish to pick a > nit (below) > Thanks David. Heh, heh. I think we might be agreeing about the phenomenon, but picking different nits to 'blame'. > On Nov

Re: [was ghc-devs] Reasoning backwards with type families

2017-12-13 Thread Clinton Mead
Hi AntC I've panicked GHC enough whilst developing Freelude so whilst I'm not sure exactly what you're saying I'd be hestiant about exploiting anything bogus (8.2 btw seems far more stable than 8.0 btw). The trick is teaching GHC to do all the type trickery it needs so you can write things like:

Re: [was ghc-devs] Reasoning backwards with type families

2017-12-13 Thread David Feuer
I still haven't really digested what you've written, but I wish to pick a nit (below) On Nov 20, 2017 3:44 AM, "Anthony Clayden" wrote: > On Thu Nov 16 01:31:55 UTC 2017, David Feuer wrote: ... > For (&&), the obvious things you'd want are ... > > There's nothing

Re: [was ghc-devs] Reasoning backwards with type families

2017-12-13 Thread Anthony Clayden
On Thu, 14 Dec 2017 at 1:55 PM, Clinton Mead wrote: > Injective Type Families are at the core of my "Freelude" package, which > allows many more types to be defined as Categories, Functors, Applicatives > and Monads. > Cool! > What would also be helpful is if

Re: [was ghc-devs] Reasoning backwards with type families

2017-12-13 Thread Clinton Mead
Injective Type Families are at the core of my "Freelude" ( https://hackage.haskell.org/package/freelude) package, which allows many more types to be defined as Categories, Functors, Applicatives and Monads. For example you can define a tuple of categories as a category and then: (f1, f2) . (g1 .

Re: [was ghc-devs] Reasoning backwards with type families

2017-12-13 Thread Anthony Clayden
On Tue, 12 Dec 2017 at 4:53 PM, Carter Schonwald wrote: > This was / perhaps still is one goal of injective type families too! I’m > not sure why the current status is, but it’s defjnitely related > Thanks Carter, yes this sort of injectiviy (semi-injectivity? partial

Re: [was ghc-devs] Reasoning backwards with type families

2017-12-11 Thread Carter Schonwald
This was / perhaps still is one goal of injective type families too! I’m not sure why the current status is, but it’s defjnitely related On Mon, Nov 20, 2017 at 3:44 AM Anthony Clayden < anthony_clay...@clear.net.nz> wrote: > > On Thu Nov 16 01:31:55 UTC 2017, David Feuer wrote: > > (Moving to

Re: [was ghc-devs] Reasoning backwards with type families

2017-11-20 Thread Anthony Clayden
> On Thu Nov 16 01:31:55 UTC 2017, David Feuer wrote: (Moving to ghc-users, there's nothing particularly dev-y.) > Sometimes it woulld be useful to be able to reason backwards > about type families. Hi David, this is a well-known issue/bit of a sore. Discussed much in the debate between type