Kind classes and associated closed type families

[Ryan Scott]

> Why does this interfere with :kind! ? It shouldn't.

Well, it seems to interfere in my usage of it, at least:

> :kind! Extract 0 '(Int, Char)
Extract 0 '(Int, Char) :: y
= ExtractPair 0 '(Int, Char)

I presumed this was because :kind! didn't do any type family reduction
whenever something was undecidable in general (to ensure :kind! always
terminates, I suppose).

Ryan S.

On Fri, Dec 18, 2015 at 10:56 AM, Richard Eisenberg <eir at cis.upenn.edu> wrote:
>
> On Dec 18, 2015, at 1:37 PM, Ryan Scott <ryan.gl.scott at gmail.com> wrote:
>
>> It hit me as to why: GHC is interpreting each Extract type instance as
>> being separate from each other, not as a part of a single, closed type
>> family over kind (a, b). And as it turns out, GHC does not allow
>> closed associated type families. [2]
>
> Yes, that's exactly right.
>
>>
>> That leads me to wonder: is there a particular reason why GHC couldn't
>> allow closed associated type families?
>
> No. At the time, we thought that associated closed type families are easy enough to build (as you do here) and just one more wrinkle that GHC didn't need. No theoretical trouble at all. Just some routine engineering, I imagine.
>
>> Because of this restriction, I
>> have to define the Extractable (a, b) instance like this:
>>
>>    instance Extractable (a, b) where
>>      type Extract n p = ExtractPair n p
>>
>>    type family ExtractPair (n :: Nat) (x :: (a, b)) :: y where
>>      ExtractPair 0 '(a, _) = a
>>      ExtractPair 1 '(_, b) = b
>>      ExtractPair _ _       = TypeError ('Text "out of bounds")
>>
>> But that requires -XUndecidableInstances, and makes it much more
>> difficult to examine type family reductions with GHCi's :kind!
>> command.
>
> Why does this interfere with :kind! ? It shouldn't. (Yes, the -XUndecidableInstances is regrettable. We really need a better type-level termination checker. Care to write one? :)  )
>
> Richard
>
>>
>> Ryan S.
>> -----
>> [1] http://dreixel.net/research/pdf/gpid.pdf
>> [2] https://downloads.haskell.org/~ghc/master/users-guide/glasgow_exts.html#synonym-families
>> _______________________________________________
>> ghc-devs mailing list
>> ghc-devs at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>