Opened 3 years ago

Closed 3 years ago

#10828 closed feature request (fixed)

TH could do a better job of representing GADTs

Reported by: spinda Owned by: jstolarek
Priority: normal Milestone: 8.0.1
Component: Template Haskell Version: 7.10.2
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: th/T10828, th/T10828a, th/T10828b
Blocked By: Blocking:
Related Tickets: #4188, #5217 Differential Rev(s): Phab:D1465
Wiki Page:

Description

For example, it's impossible to add a kind signature on a data type with DataD.

In Con I believe it's possible to encode GADT constructor signatures using NormalC (haven't tried this yet), but ideally there would be another constructor specific to GADTs to go along with RecC, InfixC, and ForallC.

Change History (21)

comment:1 Changed 3 years ago by goldfire

I believe the TH AST is fully expressive here (with one tiny caveat). It's just clunky.

Take

data T :: k -> * -> * where
  MkT :: T x Int

To encode into TH, you transform the definition to this:

data T (a1 :: k) (a2 :: *) = forall . a2 ~ Int => MkT

which has a direct translation.

The one tiny caveat is the new feature for deriving Foldable for GADTs, which distinguishes among the two forms above. (I can't find a reference to this change. Can you? It was described at Haskell Implementors' Workshop a few days ago. You, the reader, if you know the reference, please add it!)

Is it worth refactoring the TH types to handle GADTs more directly? Perhaps.

comment:2 Changed 3 years ago by goldfire

Milestone: 7.12.1

In any case, let's decide what to do and do it by the next release.

comment:3 Changed 3 years ago by spinda

re: kind signatures -- ah, you're right. It is a bit clunky, but perhaps not worth a breaking change to the structure of DataD improve. Although, if #10819 makes it in, then it could be worth slipping this in at the same time.

I hadn't heard about the new Foldable deriving feature. Any reference to that would be helpful.

comment:4 Changed 3 years ago by spinda

Summary: TH can't represent all GADTs in its ASTTH could do a better job of representing GADTs

comment:5 Changed 3 years ago by simonpj

The one tiny caveat is the new feature for deriving Foldable for GADTs, which distinguishes among the two forms above. (I can't find a reference to this change. Can you? It was described at Haskell Implementors' Workshop a few days ago. You, the reader, if you know the reference, please add it!)

See Commentary/Compiler/DeriveFunctor and #10447.

comment:6 Changed 3 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:7 Changed 3 years ago by goldfire

I think, in light of comment:5, we should add proper GADT support in TH.

comment:8 in reply to:  7 ; Changed 3 years ago by jstolarek

Owner: set to jstolarek

I can work on implementing that, but I have one question:

I think, in light of comment:5, we should add proper GADT support in TH.

Why "in light of comment:5"? I read through #10447 and I saw this example by Simon:

  data T1 a where
    MkT1 :: (a~Int) => a -> T1 a

  data T2 a where
    MkT2 :: Int -> T2 Int

  data T3 a where
    MkT3 :: (a~Int) => a -> T3 Int

All these declarations can be represented in TH:

data T1' a = a ~ Int => MkT1' a
data T2' a = a ~ Int => MkT2' Int
data T3' a = forall b. (a ~ Int, b ~ Int) => MkT3' b

It is possible to automatically derive Foldable for all three declarations T1, T2 and T3, both in GADT form as well as in the standard form given above, so DerivingFoldable makes no distinction between these three declarations. Are there other declarations where Foldable distinguishes the two forms?

Last edited 3 years ago by jstolarek (previous) (diff)

comment:9 Changed 3 years ago by jstolarek

My proposal would be to add the following constructor to Con data type:

   | GadtC Name [StrictType] [Type]

where the last field stores list of constructor indices. Once we have this new constructor I would modify DsMeta and Convert accordingly. Most importantly, GADT declarations would be now translated to use this new constructor instead of encoding that uses ForallC and NormalC.

Last edited 3 years ago by jstolarek (previous) (diff)

comment:10 in reply to:  8 ; Changed 3 years ago by goldfire

Replying to jstolarek:

It is possible to automatically derive Foldable for all three declarations T1, T2 and T3, both in GADT form as well as in the standard form given above, so DerivingFoldable makes no distinction between these three declarations.

I agree that deriving Foldable works for all of them, but does it do the same thing? I would expect not, from the commentary on #10447.

Your GadtC is missing a place for a [TyVarBndr] (to store the quantified type variables, both universals and existentials) and a Cxt to store any extra constraints. It also forbids record syntax, but maybe we can live without GADT record syntax.

comment:11 in reply to:  10 ; Changed 3 years ago by jstolarek

Your GadtC is missing a place for a [TyVarBndr] (to store the quantified type variables, both universals and existentials) and a Cxt to store any extra constraints.

My intention was to nest GadtC inside ForallC. Is there any reason why this wouldn't work?

It also forbids record syntax, but maybe we can live without GADT record syntax.

Ok, I haven't thought about that one. TBH I think I have never used (or seen) GADTs with record syntax.

comment:12 in reply to:  11 ; Changed 3 years ago by goldfire

Replying to jstolarek:

My intention was to nest GadtC inside ForallC. Is there any reason why this wouldn't work?

Good point. That would work well.

The documentation should make clear that, unlike other constructor forms, GADT constructors do not have the type variables from the declaration head in scope.

comment:13 in reply to:  12 Changed 3 years ago by jstolarek

Replying to goldfire:

The documentation should make clear that, unlike other constructor forms, GADT constructors do not have the type variables from the declaration head in scope.

Does that make a difference for TH representation (ie. GadtC data type)?

comment:14 Changed 3 years ago by goldfire

No. But it does affect the code in Convert and DsMeta.

comment:15 Changed 3 years ago by jstolarek

These are Foldable instances derived automatically for data types in comment:8

instance Foldable T1 where
  foldr f z (MkT1 a1) = f a1 z
  foldMap f (MkT1 a1) = f a1

instance Foldable T1' where
  foldr f z (MkT1' a1) = f a1 z
  foldMap f (MkT1' a1) = f a1

instance Foldable T2 where
  foldr f z (MkT2 a1) = (\ b1 b2 -> b2) a1 z
  foldMap f (MkT2 a1) = (\ b1 -> mempty) a1

instance Foldable T2' where
  foldr f z (MkT2' a1) = (\ b1 b2 -> b2) a1 z
  foldMap f (MkT2' a1) = (\ b1 -> mempty) a1

instance Foldable T3 where
  foldr f z (MkT3 a1) = (\ b1 b2 -> b2) a1 z
  foldMap f (MkT3 a1) = (\ b1 -> mempty) a1

instance Foldable T3' where
  foldr f z (MkT3' a1) = (\ b1 b2 -> b2) a1 z
  foldMap f (MkT3' a1) = (\ b1 -> mempty) a1

So DerivingFoldable does not distinguish between GADT and normal declarations - respective pairs of instances are identical. At least in this case. Perhaps there is a case where we would get different declarations?

Last edited 3 years ago by jstolarek (previous) (diff)

comment:16 Changed 3 years ago by goldfire

Good. I understood you to mean previously that the three forms had the same Foldable instance -- not that primed forms matched the unprimed forms, as you've clarified here.

So fixing this is a bit less compelling. But I still think it would be nice, given that TH is meant to reflect Haskell syntax, and it fails miserably in this corner.

comment:17 Changed 3 years ago by jstolarek

Differential Rev(s): Phab:D1465

I'll continue the discussion on Phab.

comment:18 Changed 3 years ago by jstolarek

comment:19 Changed 3 years ago by jstolarek

comment:20 Changed 3 years ago by Jan Stolarek <jan.stolarek@…>

In eeecb86/ghc:

Add proper GADTs support to Template Haskell

Until now GADTs were supported in Template Haskell by encoding them using
normal data types.  This patch adds proper support for representing GADTs
in TH.

Test Plan: T10828

Reviewers: goldfire, austin, bgamari

Subscribers: thomie, mpickering

Differential Revision: https://phabricator.haskell.org/D1465

GHC Trac Issues: #10828

comment:21 Changed 3 years ago by jstolarek

Resolution: fixed
Status: newclosed
Test Case: th/T10828, th/T10828a, th/T10828b
Note: See TracTickets for help on using tickets.