Visible Type Application
Visible Type Application, language extension TypeApplications
, allows you to give explicit type arguments to a polymorphic function; e.g. map @Int @Bool isEven xs
. Visible type application was introduced in GHC 8.0.
This the feature page that summarises status, open issues, etc.
Status
Use Keyword = TypeApplications
to ensure that a ticket ends up on these lists.
Open Tickets:
- #11349
- [TypeApplications] Create Proxy-free alternatives of functions in base
- #11350
- Allow visible type application in patterns
- #11352
- Allow applying type to label
- #11387
- Typecasting using type application syntax
- #11398
- Type application for operator sections
- #11409
- Cannot instantiate literals using TypeApplications
- #12085
- Premature defaulting and variable not in scope
- #12363
- Type application for infix
- #12446
- Doesn't suggest TypeApplications when `~` used prefix
- #12569
- TypeApplications allows instantiation of implicitly-quantified kind variables
- #12794
- Out of scope error not reported
- #13042
- Allow type annotations / visible type application in pattern synonyms
- #13512
- GHC incorrectly warns that a variable used in a type application is unused
- #13834
- Error cascade with type applications
- #14722
- Error message points to wrong location
- #15577
- TypeApplications-related infinite loop (GHC 8.6+ only)
- #15596
- When a type application cannot be applied to an identifier due to the absence of an explicit type signature, let the error just say so!
- #15782
- Visible type/kind applications in declaration of data/type constructors
- #15942
- Associated type family can't be used at the kind level within other parts of parent class
Closed Tickets:
- #11329
- Visible type applications: failing tests with WAY=hpc
- #11333
- GHCi does not discharge satisfied constraints
- #11355
- TypeApplications + RankNTypes permits "impredicativity"
- #11376
- Inconsistent specified type variables among functions and datatypes/classes when using -XTypeApplications
- #11385
- Unify named wildcards in different type applications
- #11397
- Type mismatch in local definitions in Haskell 98 code
- #11428
- ImpredicativeTypes causes GHC panic with 8.0.1-rc1
- #11431
- GHC instantiates levity-polymorphic type variables with foralls
- #11456
- Type application and :set +c command cause panic
- #11458
- Terrible failure of type inference in visible type application
- #11512
- An unwritten kind variable is "specified", when it shouldn't be.
- #11513
- Work out when GADT parameters should be specified
- #11616
- Kinds aren't instantiated
- #11638
- referring to the existential type from a GADT pattern match with a type application
- #11721
- GADT-syntax data constructors don't work well with TypeApplications
- #11947
- GHC mistakenly warns about type defaulting in the presence of -XTypeApplications
- #12025
- Order of constraints forced (in pattern synonyms, type classes in comments)
- #12033
- [TypeApplications] GHC internal error
- #12045
- Visible kind application
- #12092
- Out-of-scope variable leads to type error, not scope error
- #12093
- Wrong argument count in error message with TypeApplications
- #12220
- TypeApplications and DefaultSignatures - problems deducing type variables.
- #12371
- Error message, room for improvement
- #12411
- GHC panic on TypeApplications + TemplateHaskell
- #12529
- Error message: visible type application of constructor/variable that is not in scope
- #12565
- unhelpful error message about enabling TypeApplications
- #12601
- explicit foralls do not distinguish applicable types
- #13401
- GHCi gives conflicting information about visible type application
- #13466
- Ghci panics with type applications to unknown functions
- #13524
- GHC does not preserve order of forall'd vars with TypeApplications
- #13680
- Can't use TypeApplications with [] data constructor
- #13738
- TypeApplications-related GHC internal error
- #13819
- TypeApplications-related GHC panic
- #13846
- GHC Panic: Visible type application + function type @(_ -> _)
- #13848
- Unexpected order of variable quantification with GADT constructor
- #13853
- TypeApplications and record syntax don't mix
- #13877
- GHC panic: No skolem info: k2
- #13902
- Misleading function arity mismatch error with TypeApplications
- #13938
- Iface type variable out of scope: k1
- #13986
- TypeApplications causes parse errors in @-patterns with certain Unicode characters
- #14038
- TypeApplications regression in GHC HEAD: ‘p0’ is untouchable inside the constraints: ()
- #14348
- Poly-kinded definitions silently introduce extra type arguments captured by TypeApplications
- #14796
- Pretty Printing: GHC doesn't parenthesise (() :: Constraint)
- #15527
- TypeApplications error message doesn't parenthesize infix name
- #15568
- Kind variables in type family aren't quantified in toposorted order
- #15591
- Inconsistent kind variable binder visibility between associated and non-associated type families
- #15592
- Type families without CUSKs cannot be given visible kind variable binders
- #15793
- Type family doesn't reduce with visible kind application
- #15797
- GHC panic using visible kind application
- #15801
- "ASSERT failed!" with visible kind applications
- #15807
- GHC panic with visible kind applications
- #15816
- Visible kind applications + data family: `U :: Type' said to be of kind `k0 -> k1` in error message
Everything below here is the old wiki page. Much of it is relevant, but it needs curation. Richard will do that in due course.
Another relevant out of date page is ExplicitTypeApplication
Type Application
[Explicit] Type Application is a feature requested for Haskell that lets a programmer explicitly declare what types should be instantiated for the arguments to a function application, in which the function is polymorphic (containing type variables and possibly constraints) . Doing so essentially “short-circuits” much of the type variable unification process, which is what GHC normally attempts when dealing with polymorphic function application.
In general, Haskell’s unification algorithm is robust enough that it can do this without the programmer needing to specify explicit types. There are a few edge cases, however: see below for examples. Though some of these cases can be solved with type annotations, such annotations can be cumbersome, as the programmer needs to provide the entire signature, which can be cumbersome in complicated expressions.
It is worth noting that GHC’s intermediate language, “Core”, is fully typed and has no ambiguity - every polymorphic function application is explicitly typed. Thus, one way to think of this addition is “exposing” this feature of Core to the programmer. Indeed, once the evidence (generated by instantiating the types) is propagated to Core, it is able to be handled completely by that part of the compiler - implementing this feature did not require any changes to Core, nor to the lower-level compiler pipeline (optimizations, assembly generation, etc). See directly below for usage examples. More detailed design decisions follow the examples.
Usage:
This extension can be enabled with “TypeApplications” within the LANGUAGE pragma, or use the flag “-XTypeApplications”. The usage of this flag does not turn on any other flag implicitly. Using this flag will make a whitespace-sensitive distinction preceding each ‘@’ character: No whitespace before ‘@’ will result in an as-pattern, while having whitespace before the ‘@’ will parse as a type-application. (When this flag is turned off, the behavior is the same as it is now - no whitespace sensitivity). See Design with more information on the syntax.
Here are some examples where type application is useful:
This test case shows how using explicit type application resolves ambiguity, by using the infamous "show/read" problem as an example. (The show/read problem is a problem in which the answer to using show followed by read - 'show (read "3")' should be obvious, but fails in the typechecker because of an ambiguity in the constraints). Using type application on either of the functions, or both, allows the compiler to correctly typecheck the program.
answer_read = show (read @Int "3") -- "3" :: String answer_show = show @Integer (read "5") -- "5" :: String answer_showread = show @Int (read @Int "7") -- "7" :: String
A more difficult example involves type families, which are generally difficult to infer, and this creates problems when attempting to unify types involving type families. In this specific example, the declaration "g False" would be ill-typed [since it has no type signature], but adding the explicit type “@Char” will resolve this problem.
type family F a type instance F Char = Bool g :: F a -> a g _ = undefined f :: Char f = g True h = g False -- will cause an error h' = g @Char False
One does not need to have the “-XExplicitForAll” extension turned on to use “-XExplicitTypeApplication”. Without the forall flag, generally types will be inferred by simply stacking all of the foralls at the beginning. You can also leave off explicit types by simply withholding the annotation, or by providing “@_” to let the typechecker instantiate the variable regularly. This is particularly useful when you want to provide a type to the first and third type variable, but not the second, for example:
-- Will be treated as: -- forall a b c d. a -> b -> c -> d -> (a, b, c, d)... quad :: a -> b -> c -> d -> (a, b, c, d) quad w x y z = (w, x, y, z) foo = quad @Bool @_ @Int False 'c' 17 "Hello!" -- Char and [Char] will be inferred for type variables ‘b’ and ‘d’.
This also works with types of arbitrary kinds, including with kind variables. (There is no explicit kind application yet, but with the current implementation, it is very easy to extend it in the future). Of course, the types within the type applications will have to satisfy the kinds you are providing.
data Two (a :: * -> k) = T two :: Two a -> Int two _ = 2 twoBase = two T twoOk = two @(Either Int) T twoBad = too @Maybe (T :: Two Either)
Design
There are several small design questions that can be asked of Explicit Type Application. Below are the questions and the decisions that were made:
- Is a type annotation and/or signature required for a function in order to use type applications when applying it?
No. Haskell generalizes certain functions, with a simple, straightforward signature; all the type variables are at the top, and it is a fairly simple signature to instantiate and work with.
- Should we require a forall in the signature?
No, for similar reasons as above. Additionally, we did not want to create a dependency on the "ExplicitForAll" flag, and wanted type applications to be a small, surgical feature that has as few side effects as possible.
- What order is used to instantiate the type variables?
Left-to-right order of the type variables appearing in the foralls. This is the most logical order that occurs when the instantiation is done at the type-variable level. Nested foralls work slightly differently, but at a single forall location with multiple variables, left-to-right order takes place. (See below for nested foralls).
- How will it work with partial function application? Will we allow: leaving out arguments in function application, but allow type application to de-generalize the expression?
Yes. This will allow the programmer to use the partially applied the function later, but only to arguments with specific types. This could be useful for a library designer, to use a generalized function internally, and only expose a specialized version of that function in the interface.
- Wildcard Application
Allows the programmer to not instantiate every type variable if they do not want to. Example
f xs = reverse @ (Maybe _) xs -- Instantiates reverse at a Maybe type -- but lets GHC infer which
An explicit application@ _
is just like the implicit form: instantiate with a fresh unification variable.
- Named wildcards. Can you write
f xs = reverse @ (_a -> _a) xs
The intent here is that_a
stands for a type, but not necessarily a type variable.
- Should non-prenex-form functions be allowed to use type applications? If so, how should we allow it?
Yes. We allow this by requiring that type application appear where the forall is located in the type. See the following example:
many :: forall a b. a -> b -> forall c. [c] -> forall d . Num d => d -> (a, b, [c], d) many a b c d = (a, b, c, d) foo = many @Int @Bool 5 True @Char "hello" @Float 17
- Concrete Syntax:
We choose to use the ‘@’ symbol, as this is the symbol that is used in Core, GHC’s intermediate language. Turning on this extension will make the ‘@’ symbol whitespace-sensitive in the front: whitespace before an ‘@’ will parse as a type-application, while no whitespace in front of the ‘@’ will parse as an as-pattern. This is similar to the way ‘.’ behaves differently with whitespace (function composition vs. module naming), but note that the only whitespace sensitivity occurs ‘’’before’’’ the ‘@’ and not after. Additionally, when the extension is off, there is no change in current behavior and no whitespace sensitivity.