Hetero-kinded eqT

[phadej]

Currently we have

eqT :: forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)

But we could have hetoro-kinded version:

heqT :: forall (a :: k1) (b :: k2). (Typeable a, Typeable b) => Maybe (a :~~: b)

That can be implemented safely using eqTypeRep today, but that is indirect.

Should the new combinator be added, what should it be named? heqT is suggested.

EDIT 2022-10-28: Also export eqT and heqT from Type.Reflection. Currently eqT is exported only from Data.Typeable.

cc @RyanGlScott

[treeowl]

Sorry for my last comment. Read you wrong.

[Bodigrim]

I never touched eqT and don't really know how useful is the proposed generalization. Could someone more experienced in this area please chime in?

[treeowl]

I have no idea how useful it would be, but I think heqT wouldn't be a bad name.

[ramirez7]

eqTK?

[Lysxia]

+1 for heqT. I don't know of a real use case off hand but it seems quite plausibly useful.

[tomjaguarpaw]

I don't know of a real use case off hand

Can we please see a real use case before we vote on this?

[phadej]

I don't know any "real" use case. I just noticed that the API is not complete.

[ekmett]

@tomjaguarpaw: Usecases mostly revolve around EDSLs for generics / scrap-your-boilerplate that don't get stuck only dealing with Type or k -> Type.

We're paying the price for Axiom K, we might as well make it more usable.

+1 for heqT.

[tomjaguarpaw]

Sure, I understand the use case of the general functionality, but we already have eqTypeRep. The difference is just about whether we provide the TypeRep arguments explicitly or whether we conjure them up using a Typeable constraint. I'm not sure why one would prefer one rather than the other.

[Bodigrim]

I must admit that I never used eqTypeRep as well, so don't really have an informed opinion to vote for or against. I'm happy to be persuaded (either way) by users of Type.Reflection.

[RyanGlScott]

As an occasional Type.Reflection user, the biggest draw of heqT for me (aside from API consistency) is the chance to cut out a fair bit of boilerplate code. Currently, you have to write something like eqTypeRep (typeRep @a) (typeRep @b) if you want to compare two types a and b for equality heterogeneously. This is doable, but rather verbose. With heqT, this would simply become heqT @a @b.

[phadej]

FWIW. I'd amend the proposal with (hopefully trivial) addition to export eqT and heqT from Type.Reflection as well.

As a potential Type.Reflection user I'd find it strange to import Data.Typeable (Type.Reflection exports Typeable class already for example).

[ekmett]

@tomjaguarpaw

Yes, you can assemble it. One might even argue that this simple combinator falls below the Fairbairn threshold,

heqT = eqTypeRep typeRep typeRep

is a trivial application of things that already exist. All of that is true.

But we're already well off to the side in Type.Reflection, or well, somewhat less so in Data.Typeable. I'm not too worried about taking up a rarified name like this, and it seems best to provide the hook for someone who does come looking for the thing, especially given that I think it is desirable to make (:~~:) feel consistent with (:~:) and eqT already exists, lest users have to memorize trivial inessential distinctions between (:~:) and (:~~:), like the conspicuous lack of such a function that exists in its peer.

I'd argue most users of Typeable don't think about TypeReps.

[treeowl]

I'd argue most users of Typeable don't think about TypeReps.

@ekmett, I haven't used Typeable all that much, but when I have, I've almost always thought about TypeReps. I expect that will be more common for people coming to it after Type.Reflection.

[ekmett]

@ekmett, I haven't used Typeable all that much, but when I have, I've almost always thought about TypeReps. I expect that will be more common for people coming to it after Type.Reflection.

My guiding star is that Typeable mostly (originally) existed to support Data, and Data, despite offering a combinator irrelevantly named dataTypeRep, literally never mentions a word about TypeRep, an implementation detail of Typeable, and one we fundamentally changed by creating Type.Reflection and making now two incompatible notions of TypeRep that you have to messily work with qualified, etc.

Data.Data is littered with dozens of combinators like

dataCast1 :: (Data a, Typeable t) => (forall d. Data d => c (t d)) -> Maybe (c a)

with no TypeReps ever used or offered. Why? Admittedly, the origin of this is that Typeable a contained more information than the unparameterized TypeRep constraints in the world before :~~: came along and made it possible for us to express TypeRep a in Type.Reflection! and so there was no way to write equivalent combinators that took TypeReps in the before times. Heck, if you go far enough back you used to have Typeable1, Typeable2, etc. to deal with. the old solutions were bad bad bad.

So, yes, I agree, with Type.Reflection in hand, thinking in terms of TypeReps is at least no longer actively harmful.

[Lysxia]

We could have an API for Typeable without any explicit TypeRep, at no loss of expressiveness for users. TypeRep would remain as an implementation detail, and as an escape hatch for temporarily missing features from the Typeable API. At the moment, such an API is missing heqT.

The state of mind for one using heqT is "I want to compare two types." And arguably the two types are all the information needed from one writing the code and for one reading it. Having to pass the Typeable constraint through an explicit typeRep call is an extraneous step which also breaks an abstraction barrier as explained above.

A plausible use case for heterogeneous equality tests: heqT/eqTypeRep is necessary to write a function like "check whether a type a is of the form Maybe t for any t". Indeed, the obvious way to do this is to use the App pattern to split a into m t, and then call heqT @m @Maybe. This is a heterogeneous comparison because at this point, we only know that m has kind k -> *, for some existential k also introduced by App. This technique could be used for SYB metaprogramming on type-indexed ASTs (e.g., if you have Term t for "terms of type t", this lets you apply an optimization to all subterms, which are Term but not necessarily of the same type t).

{-# LANGUAGE ScopedTypeVariables, AllowAmbiguousTypes, TypeApplications, GADTs, PolyKinds #-}
module A where

import Type.Reflection
import Data.Typeable (eqT)

isMaybe :: forall a. Typeable a => a -> Bool
isMaybe _ = case typeRep @a of
  App (f :: TypeRep f) _ -> withTypeable f (    -- I blame the lack of first-class existential quantification for this line
    -- case eqT @f @Maybe typeRep typeRep) of   -- eqT doesn't work here,
    case heqT @f @Maybe of                      -- heqT does
      Just _ -> True
      Nothing -> False)

heqT :: forall a b. Typeable a => Typeable b => Maybe (a :~~: b)
heqT = eqTypeRep typeRep typeRep

Admittedly, the usefulness of App here takes away from the point I made just before about TypeRep being useless in a user-level API, but I would counter that it's still not strictly necessary---it could be replaced with a function with Typeable constraints in weird places---and it being so useful is more a symptom of poor support for existential quantification, which would otherwise be expected from a self-respecting dependently typed language.

[tomjaguarpaw]

Very nice! So the moral of the story is that we prefer to pass types-with-constraints around, not singletons. I don't understand your point about App and existentials though. If App also obeyed the moral of the story, and bound types not singletons, then your example would look much nicer. Does it still need existentials? If so, could you explain? I don't get it.

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}

-- | Requires GHC 9.4
module A where

import Data.Kind (Type)
import Data.Typeable (eqT, Proxy(Proxy))
import Type.Reflection (Typeable, (:~~:), withTypeable, eqTypeRep)
import qualified Type.Reflection as R

isMaybe :: forall (a :: Type). Typeable a => Bool
isMaybe = case typeRep @a of
  App @f @_  ->
    case heqT @f @Maybe of
      Just _ -> True
      Nothing -> False
  _ -> False

-- Proposed combinator
heqT :: forall a b. Typeable a => Typeable b => Maybe (a :~~: b)
heqT = eqTypeRep R.typeRep R.typeRep

-- (Part of) what TypeRep could have been
data TypeRep a where
  App :: forall {k2} {k1} (f :: k1 -> k2) (b :: k1). (Typeable f, Typeable b) =>
    TypeRep (f b)
  Other :: TypeRep a

-- typeRep for what TypeRep could have been
typeRep :: forall a. Typeable a => TypeRep a
typeRep = case R.typeRep @a of
  R.App (f :: R.TypeRep f) (x :: R.TypeRep x) ->
    withTypeable f $
      withTypeable x $
        App
  _ -> Other

On the other hand I discovered some very surprising behaviour around trying to bind types.

Tangentially, App seems sadly weaker than it could be. For Typeable (f a) where f :: k1 -> k2 and a :: k1 it doesn't give us TypeRep k2 even though it's there in the TrApp constructor :(

[tomjaguarpaw]

it doesn't give us TypeRep k2

Though I suppose we can obtain that from typeRepKind.

[Lysxia]

You did answer the issue I was thinking of. I didn't realize we could already bind variables like this, App @f @_.

[tomjaguarpaw]

Yes, it's amazingly cool, and only available from 9.4 I believe.

[Bodigrim]

@phadej could you please raise a draft MR?

[phadej]

MR: https://gitlab.haskell.org/ghc/ghc/-/merge_requests/9441

[Bodigrim]

Dear CLC members, let's vote on the proposal to add Data.Typeable.heqT :: (Typeable a, Typeable b) => Maybe (a :~~: b) as detailed in https://gitlab.haskell.org/ghc/ghc/-/merge_requests/9441/diffs.

---

+1 from me.

[Bodigrim]

CC @tomjaguarpaw @chessai @cgibbard @emilypi @mixphix

[tomjaguarpaw]

+1

[emilypi]

+1

[mixphix]

+1

[cgibbard]

+1

[Bodigrim]

Thanks all, 5 votes out of 6 possible are anough to approve.

[chshersh]

I'm trying to summarise the state of this proposal as part of my volunteering effort to track the progress of all approved CLC proposals.

Field	Value
Authors	@phadej
Status	merged
base version	4.18.0.0
Merge Request (MR)	https://gitlab.haskell.org/ghc/ghc/-/merge_requests/9441
Blocked by	nothing
CHANGELOG entry	present
Migration guide	not needed

Please, let me know if you find any mistakes 🙂