[Haskell-cafe] data kinds and exhaustiveness of typeclass instances

[Paul Brauner]

Another way of putting it, please correct me if I'm wrong. In coq we could
prove forall a, C (Foo a) by case analysis on a. Then we could use that
proof to recover the f by applying it to p inside g. It can't work in
Haskell because p has no runtime representation. In Haskell the proxy plays
the role of p, KnownTag plays the role of the proof that p can be
eliminated, and "instance KnownTag a => C (Foo a)" plays the role of the
theorem.

On Tue, Mar 2, 2021 at 8:23 PM Paul Brauner <polux2001 at gmail.com> wrote:

> Thanks all, this all makes sense!
>
> On Tue, Mar 2, 2021 at 4:34 PM Seph Shewell Brockway <seph at codex.scot>
> wrote:
>
>> On Tue, Mar 02, 2021 at 03:00:55PM +0000, Richard Eisenberg wrote:
>> > > Is there a way to somehow convince GHC of that fact so that g
>> typechecks?
>> >
>> > No.
>> >
>> > First, it would actually be unsound to do so, because of the
>> possibility of exotic types, built with pathological combinations of type
>> and data families: https://gitlab.haskell.org/ghc/ghc/-/issues/14420 <
>> https://gitlab.haskell.org/ghc/ghc/-/issues/14420>
>> >
>> > But, actually, the bigger problem is that we need a class constraint in
>> order to allow a function to compute at runtime. The function f actually
>> takes two arguments at runtime: a representation of the instance which
>> carries f's implementation (this is sometimes called a dictionary), and the
>> normal argument of type a. `g`, on the other hand, has no access to the
>> dictionary needed at runtime, and so it's unclear how it should compute.
>> >
>> > Put another way: a value of type Foo carries no information (beyond the
>> fact that it terminates), because Foo has only one data constructor. So
>> there's no way that g :: Foo a -> Int could be anything but a constant
>> function. You need the class constraint to change this fact.
>> >
>> > Hope this helps!
>> > Richard
>>
>> To elaborate a little on Richard’s answer, this is the reason for
>> GHC.TypeLits’ KnownNat class, so that we have
>>
>> natVal :: KnownNat n => proxy n -> Integer
>>
>> You’d have to supplement your program with a class KnownTag, like so:
>>
>> data Tag = A | B
>> data Foo (a :: Tag) = Foo
>>
>> class KnownTag (a :: Tag) where
>>   tagVal :: proxy a -> Tag
>>
>> instance KnownTag A where
>>   tagVal _ = A
>>
>> instance KnownTag B where
>>   tagVal _ = B
>>
>> class C a where
>>   f :: a -> Int
>>
>> instance KnownTag a => C (Foo a) where
>>   f _ = case tagVal (Proxy :: Proxy a) of A -> 1; B -> 2
>>
>> g :: KnownTag a => Foo a -> Int
>> g = f
>>
>>                                              Regards,
>>
>>                                              Seph
>>
>> --
>> Seph Shewell Brockway, BSc MSc (Glas.)
>> Pronouns: she/her
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210302/b7d8bbb3/attachment.html>