type-application.md

+## 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. 
+
+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:**
+---
+
+## **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.
@@ -71,4 +75,52 @@ two _ = 2
 twoBase = two T
 twoOk = two @(Either Int) T
 twoBad = too @Maybe (T :: Two Either)
-```
\ No newline at end of file
+```
+
+---
+
+## **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. See the examples section (above) for a use case.
+
+- *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:
+
+```wiki
+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.