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

[Paul Brauner]

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/8a7a55d3/attachment.html>