Skip to content

Instantly share code, notes, and snippets.

@RyanGlScott RyanGlScott/KindOf.md
Last active Mar 20, 2019

Embed
What would you like to do?
KindOf is a crazy, crazy type.

I've discovered something how to do something that GHC never intended you to be able to do, and I'm wondering if there's a way to abuse this to do interesting things.

It's known that you can express visible, dependent quantification at the kind level:

data A a :: a -> Type
λ> :kind A
A :: forall a -> a -> Type

However, you can't express visible, dependent quantification at the type level... or so I thought. There's this interesting type that you can write which is often called KindOf:

type family KindOf (a :: k) :: Type where
  KindOf (a :: k) = k

Here's an interesting question: what is KindOf A? Normally, this is a thought that GHC won't let you think:

λ> :kind KindOf A

<interactive>:1:8: error:
    • Expected kind ‘k0’, but ‘A’ has kind ‘forall a -> a -> Type’
    • In the first argument of ‘KindOf’, namely ‘A’
      In the type ‘KindOf A’

However, this is only a small hurdle. It turns out that we can lift this restriction by enabling the ImpredicativeTypes extension!

λ> :set -XImpredicativeTypes
λ> :kind! KindOf A
KindOf A :: Type
= forall a -> a -> Type

One consequence of this is that we can use KindOf A at the type level. That is to say, we can have visible, dependent quantification at the type level, despite my earlier claim to the contrary!

f :: KindOf A
f = undefined
λ> :type +v f
f :: forall a -> a -> Type
λ> :type f
f :: forall a -> a -> Type

This is pretty interesting, since GHC certainly never intended for this to be possible (at least, not at the moment). The question is: can we abuse this feature to make GHC do crazy things?

So far, I haven't been able to come up with anything terribly interesting. Here are the two things of (minor) note that I've discovered so far:

  1. Let's say you define two functions on top of f like so:

    f :: KindOf A
    f = undefined
    
    g = f
    
    h = g

    What are the types of g and h? To my surprise, they're actually different:

    $ ghci Bug.hs -fprint-explicit-foralls -XNoStarIsType
    GHCi, version 8.6.1: http://www.haskell.org/ghc/  :? for help
    Loaded GHCi configuration from /home/rgscott/.ghci
    [1 of 1] Compiling Main             ( Bug.hs, interpreted )
    
    Bug.hs:24:1: warning: [-Wmissing-signatures]
        Top-level binding with no type signature:
          g :: forall a -> a -> Type
       |
    24 | g = f
       | ^
    
    Bug.hs:26:1: warning: [-Wmissing-signatures]
        Top-level binding with no type signature:
          h :: forall {a}. a -> Type
       |
    26 | h = g
       | ^
    

    Kind of weird.

  2. Are there any other implementations of f? Unfortunately, it appears that the answer is "no". Here's another thing that I half-heartedly expected to typecheck:

    f :: KindOf A
    f _ = undefined

    Alas, GHC doesn't play along with me:

        • Couldn't match type ‘p0 -> a0’ with ‘forall a -> a -> Type’
          Expected type: KindOf A
            Actual type: p0 -> a0
        • The equation(s) for ‘f’ have one argument,
          but its type ‘KindOf A’ has none
       |
    22 | f _ = undefined
       | ^^^^^^^^^^^^^^^
    

    However, this isn't the full story. It turns out that the way that KindOf is defined is important here. In the example above, I was using a KindOf type family (whose definition I showed earlier). On the other hand, if you define KindOf as a type synonym:

    type KindOf (a :: k) = k

    Then you actually can implement f _ = undefined! What's more, its type seems to change in a subtle way... at least, according to GHCi:

    λ> :type +v f
    f :: KindOf A
    λ> :type f
    f :: forall {a}. a -> Type
    

    Also, the type of g apparently changes:

    $ ghci Bug.hs -fprint-explicit-foralls -XNoStarIsType
    GHCi, version 8.6.1: http://www.haskell.org/ghc/  :? for help
    Loaded GHCi configuration from /home/rgscott/.ghci
    [1 of 1] Compiling Main             ( Bug.hs, interpreted )
    
    Bug.hs:26:1: warning: [-Wmissing-signatures]
        Top-level binding with no type signature:
          g :: forall {a}. a -> Type
       |
    26 | g = f
       | ^
    
    Bug.hs:28:1: warning: [-Wmissing-signatures]
        Top-level binding with no type signature:
          h :: forall {a}. a -> Type
       |
    28 | h = g
       | ^
    

    Odd stuff.

Despite my best efforts, these are the only interesting things that I'm able to do with this trick. I feel like I've only scratched the surface here, though, and perhaps more creative minds can put this idea to better use.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.