Provide a primitive to show types as Symbols

[isovector]

ShowType has an annoyingly specific kind: k -> ErrorMessage. If we had something similar whose kind were instead k -> Symbol, we could use it in many more places.

Rendered

[treeowl]

My first thought was that yes, of course we should do something like this! Then I realized that one could easily construct a program that only compiles if GHC formats a type in a particular way. Hrmm.

Then my biggest concern hit. TypeError ('ShowType t) is really quite magical: it can show polymorphic types. This is a lot of the power it has over showing a TypeRep, I think. If you have a ShowType type family, how exactly will inference work? That sounds complicated!

[goldfirere]

@treeowl, I don't quite see what the complicated inference case would be.

My concern is more around @treeowl 's first concern, about compilation depending on GHC's choice for rendering types.

I'm also lost at the proposal's "it will emit a derived constraint KnownSymbol (ShowTypeSymbol a)". What does that mean in practice?

[treeowl]

@goldfirere, I don't have a fully worked example. My concern is that someone may try to show a type that has metavariables in it. What's supposed to happen then? If the result depends on details of the type checking process, that sounds much too wild to me. What if the result of showing the type somehow determines the values of one or more of those variables? If that's possible, it sounds twisted.

[goldfirere]

I'm assuming that ShowTypeSymbol reduces only when it encounters a concrete type. That is ShowTypeSymbol [a] would be stuck until we learn what a is.

[treeowl]

@goldfirere, that seems like an eminently reasonable restriction. It is, however, quite different from what TypeError can support. This mechanism could not be used to implement the 'ShowType case of TypeError.

[goldfirere]

Good point -- this new feature couldn't be used to implement today's TypeError. Note that the problem is just one of type inference, if ShowTypeSymbol a reduces to a different symbol than ShowTypeSymbol Int, we've lost type safety.

[isovector]

@treeowl @goldfirere thanks for your comments. Would you be more supportive of the proposal if it came with a specification for how the type were printed, an if ShowTypeSymbol worked only for concrete types?

[treeowl]

@isovector, that would certainly help. You'll also either have to ban higher-rank types or specify precisely how to deal with them. I think you should also remove the claim that this can be used to implement TypeError; otherwise we'd have to cripple the latter.

[isovector]

@treeowl: the requested changes have been made. PTAL when you have a chance. Thanks to @Lysxia for helping me with the correct behavior for this specification.

[parsonsmatt]

I would greatly appreciate this feature. I've often wanted to have a type-level set backed by a sorted type-level list, and have been unable to do so as Type's aren't comparable (while Symbols are). Being able to automatically translate between the two would allow me to write that library.

[int-index]

@parsonsmatt No, you would erroneously equate types which have equal names but come from different modules/packages. What you want is type-level fingerprinting à la Typeable.

[isovector]

@nomeata ready for committee eyes. Thanks!!

[goldfirere]

Before making a recommendation to the committee, I have a few questions: 1. Let's suppose that every Haskeller who wrote a type definition also wrote type instances for `ShowTypeSymbolPrec`, both for the type itself and for any promoted data constructors. Then could this be all implemented in user-land, just with ordinary type families? I foresee needing an infinite number of instances to deal with Symbols and Nats, as well as some magic around the differentiation between lists/tuples and other constructors. Otherwise, it looks possible. Do you agree? 2. Presumably, this feature would look through type synonyms. (Anything else would break type safety.) So, `ShowType String` yields `[Char]`. This has the potential to break abstraction barriers, allowing packages to see how other packages implement their (abstract) types. This means that a package that believes it's upholding the PVP might inadvertently cause downstream breakage when performing a (supposedly purely internal) refactor. Do you agree? 3. How does ShowType deal with types that are not in scope? This could happen because the types were inferred, or due to type synonym/type family expansion. We can't have ShowType behave differently in different modules, so it would have to either (A) render every type with its package and module prefix or (B) always omit package and module prefixes. Choice (B) is much more pleasant to use, but it's potentially ambiguous, if there are multiple types of the same name in play. What are your thoughts here? Thanks!

[Lysxia]

Replying to point 2: Shouldn't changing a type synonym be considered a breaking change? Are you thinking about a more complex situation?

[treeowl]

I agree with @Lysxia. Type synonyms aren't a proper abstraction mechanism anyway.

[treeowl]

@goldfirere, I think we want ShowType to show the unqualified name. But we can add primitives to get and show the module and package names.

[isovector]

1. Yes, this can all be implemented in user land minus the magic for built-in datakinds. That being said, many of the type instance rules given in the proposal overlap, so it wouldn't be as easy as just giving instances for type constructors and importing a module for the rest.

2. I agree that ShowType should look through type synonyms. It also seems to me that changing a type synonym should be considered a breaking change, but the PVP specification is rather quiet on this front.

3. It seems like we should always show an unqualified name. Getting package and module names could be given by some other primitive of kind k -> (Symbol, Symbol). Having access to these would help @parsonsmatt's earlier example. I suspect the majority of use-cases for ShowTypeSymbol wouldn't care about this information, but I'm willing to add it to the proposal.

[Lysxia]

What if instead of ShowTypeSymbol, GHC provides a primitive for "atomic types" (Maybe, [], as opposed to Maybe (), [Int]).

type family TypeInfoOf (a :: k) :: TypeInfo

-- Compiler-generated
type instance TypeInfoOf Maybe = 'NormalData "base" "GHC.Maybe" "Maybe"
type instance TypeInfoOf (:*:) = 'InfixData ('Infixr 6) "base" "GHC.Generics" ":*:"
-- etc.

data TypeInfo
  = NormalData Symbol Symbol Symbol
  | InfixData ...
  | Symbol Symbol
  | Nat Nat
  -- ... special cases for tuples, []?

With a magic instance for Nats, maybe also for Symbols.

Given only TypeInfoOf, it seems feasible to define multiple versions of ShowTypeSymbol in libraries, in particular both one that shows unqualified names, and another with fully package-qualified names.

I think we can already approximate that using Generic, but there are no instances for GADTs.

---

ShowType has an annoyingly specific kind: k -> ErrorMessage. If we had something similar whose kind were instead k -> Symbol, we could use it in many more places.

ShowType is unnecessarily restricted to only being useable in custom type error contexts. Slightly changing its kind would allow it to be used in many more places.

The proposal suggests that it generalizes the current ShowType, but as @treeowl mentioned earlier, ShowType does quite a bit of magic that justifies restricting it to error messages only. The difference seems worth mentioning in the actual proposal.

[int-index]

I support @Lysxia idea of TypeInfo, and I'd like it to include Fingerprint which would be equal to the one in TypeRep. This would make it possible to sort types and define type-level sets (as @parsonsmatt mentioned).

[isovector]

I spent a good chunk of yesterday playing around with TypeInfo, and it does indeed seem to solve the use-cases better than my original proposal. I'll try to update it in the next few days.

edited a few times: @int-index there's a bit of a problem with adding Fingerprints, namely that my understanding of @Lysxia's suggestion is that it pushes actually doing anything with TypeInfos to library code. As a result, we can get Fingerprints for type constructors, but crucially not for arbitrary types. If you have any suggestions about how to make this work, I'd be all ears!

[goldfirere]

Thanks for the clarifications @isovector. Yes, I was just wrong about my point (2) on type synonyms -- sorry!

I would be ready to make my recommendation to the committee here, but it seems like more revisions are in the works. I'll wait until things settle down again.

[goldfirere]

As this has planned updates, I've removed the "under review" label. Please resubmit when ready.

[isovector]

Based on @Lysxia's suggestion, I've come up with the following formulation. Wondering if anyone has feedback on this before I go through the work of updating the proposal proper.

{-# LANGUAGE DataKinds    #-}
{-# LANGUAGE PolyKinds    #-}
{-# LANGUAGE TypeFamilies #-}

module Proposal where

import           GHC.Generics (FixityI (..), Associativity (..))
import qualified GHC.TypeLits as TL

data Datatype = Datatype
  { datatypeName   :: TL.Symbol
  , datatypeFixity :: FixityI
  , moduleName     :: TL.Symbol
  , packageName    :: TL.Symbol
  , isNewtype      :: Bool
  }

data Constructor = Constructor
  { conName     :: TL.Symbol
  , conFixity   :: FixityI
  , conDatatype :: Datatype
  }

data TypeInfo
  = Data     Datatype
  | Promoted Constructor
  | Symbol   TL.Symbol
  | Nat      TL.Nat

type family TyRep (t :: k) :: TypeInfo
type family ShowSymbol (t :: TL.Symbol) :: TL.Symbol
type family ShowNat    (t :: TL.Nat)    :: TL.Symbol

In particular, the proposal would be to provide the bottom three type families as GHC primitives, and relegate the work of showing more complicated types to be built out of these in library code.

[int-index]

@isovector How are you going to represent Either Int here? Your TypeInfo is missing constructor application, App TypeInfo TypeInfo.

I suggest following the structure of TypeRep:
https://hackage.haskell.org/package/base-4.12.0.0/docs/src/Data.Typeable.Internal.html#TypeRep

[goldfirere]

I understand that you can skip type families here, but what about data families? Classes? Functions? I worry that this will spiral out of control and end up replicating the existing features of generics...

[jvanbruegge]

I want to add that I would really like to see GHCi using this type family for :type, so you can provide easier to look at type printing. Maybe the current behavior could be moved to :type! to see behind the scenes

[Lysxia]

@jvanbruegge that seems unlikely since ShowType will only resolve to a concrete string for fully instantiated, monomorphic types, whereas :type should handle the whole of Haskell's type language, including quantifiers and type synonyms (it seems undesirable to have them expanded by default, which ShowType would most likely do).

[isovector]

Closing this for personal reasons---if anyone else would like to take up the mantle, that'd be cool!