GHC extension - TypeApplications

Providing type arguments explicitly

Learning more about type level programming has been something on my list of to dos for a while now, so I decided to start by looking at one of the many GHC extensions required for the job - TypeApplications. Let's look at the classic polymorphic function example: id, the identity function (I'm loading ghci with some additional command line options to display Core)

$ ghci

λ> id x = x

==================== Tidy Core ====================
Result size of Tidy Core
  = {terms: 18, types: 12, coercions: 0, joins: 0/0}

-- RHS size: {terms: 3, types: 3, coercions: 0, joins: 0/0}
id :: forall p. p -> p
id = \ (@ p) (x :: p) -> x

Here we can see that id receives an implicit type variable @p, which represents the polymorphic type. With polymorphic function application, GHC deals with most of the unification process without the programmer needing to get involved. There are however, many examples of ambiguity; usually these are resolved with type annotations, but they can grow gnarly. In many Haskell libraries, you may have seen the following workaround: prior to GHC 8, controlling type variable instantiation meant using the Proxy type, which is a type that holds no data but is used to provide type information:

module NoTypeApp where

import Data.Proxy

data Foo = Foo
  deriving (Read, Show)

data Bar = Bar
  deriving (Read, Show)

foo :: String -> String
foo x = show ((read :: String -> Foo) x)

  :: forall a . (Show a, Read a)
  => Proxy a
  -> String -> String
polyReadThenShow _ x = show ((read :: String -> a) x)

foo' :: String -> String
foo' = polyReadThenShow (Proxy :: Proxy Foo)

bar :: String -> String
bar = polyReadThenShow (Proxy :: Proxy Bar)

An obvious application of the TypeApplications extension is that we can rewrite the above without the need for phantom typing:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module HasTypeApp where

data Foo = Foo
  deriving (Read, Show)

data Bar = Bar
  deriving (Read, Show)

  :: forall a . (Show a, Read a)
  => String -> String
polyReadThenShow = show . read @a

foo :: String -> String
foo = polyReadThenShow @Foo

bar :: String -> String
bar = polyReadThenShow @Bar

This is of course, a rather trivial/dumb use; this would be more useful in scenarios like resolving ambiguity in type classes or type families. But while we're at it, here's another dumb example that demonstrates a trivial case of type ambiguity:

-- adding on to the earlier example
-- class Qux a b where
--   qux :: String

-- instance Qux Foo Bar where
--   qux = "foo"

-- in ghci
λ> qux
<interactive>:28:1: error:
    * Ambiguous type variables `a0', `b0' arising from a use of `qux'
      prevents the constraint `(Qux a0 b0)' from being solved.
      Probable fix: use a type annotation to specify what `a0',
                                                          `b0' should be.
      These potential instance exist:
        instance [safe] Qux Foo Bar -- Defined at src/HasTypeApp.hs:29:10
    * In the expression: qux
      In an equation for `it': it = qux

λ> qux @Foo @Bar

If this interests you, you should check out the paper Visible Type Applications (Extended version).

<< back