type-application.md

 
-This page talks about Type Application within function expressions, in which the function is polymorphic and the type application instantiates one or more of the types when typechecking the function.
+\[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 “[ExplicitTypeApplication](explicit-type-application)” within the LANGUAGE pragma, or use the flag “-XExplicitTypeApplication”. 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.
+
+```wiki
+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.
+
+```wiki
+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:
+
+```wiki
+-- 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.
+
+```wiki
+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)
+```
\ No newline at end of file