From 3099e40d2737172c746a6456ddcd34b54e120aa0 Mon Sep 17 00:00:00 2001 From: "Iavor S. Diatchki" Date: Mon, 17 Mar 2014 23:19:16 -0700 Subject: Add some documentation about type-level literals. I moved the "promoted literals" sub-section into a separate section, as many folks were not finding the docs. I also added some additional paragraphs describing the current state of the feature. --- docs/users_guide/glasgow_exts.xml | 178 +++++++++++++++++++++++++++++--------- 1 file changed, 135 insertions(+), 43 deletions(-) (limited to 'docs') diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml index 9dbd545069..33124122ef 100644 --- a/docs/users_guide/glasgow_exts.xml +++ b/docs/users_guide/glasgow_exts.xml @@ -6590,14 +6590,78 @@ Note that this requires . - - -Promoting existential data constructors + +Runtime Values for Type-Level Literals -Note that we do promote existential data constructors that are otherwise suitable. -For example, consider the following: +Sometimes it is useful to access the value-level literal assocaited with +a type-level literal. This is done with the functions +natVal and symbolVal. For example: -data Ex :: * where - MkEx :: forall a. a -> Ex +GHC.TypeLits> natVal (Proxy :: Proxy 2) +2 -Both the type Ex and the data constructor MkEx -get promoted, with the polymorphic kind 'MkEx :: forall k. k -> Ex. -Somewhat surprisingly, you can write a type family to extract the member -of a type-level existential: +These functions are overloaded because they need to return a different +result, depending on the type at which they are instantiated. -type family UnEx (ex :: Ex) :: k -type instance UnEx (MkEx x) = x +natVal :: KnownNat n => proxy n -> Integer + +-- instance KnownNat 0 +-- instance KnownNat 1 +-- instance KnownNat 2 +-- ... -At first blush, UnEx seems poorly-kinded. The return kind -k is not mentioned in the arguments, and thus it would seem -that an instance would have to return a member of k -for any k. However, this is not the -case. The type family UnEx is a kind-indexed type family. -The return kind k is an implicit parameter to UnEx. -The elaborated definitions are as follows: +GHC discharges the constraint as soon as it knows what concrete +type-level literal is being used in the program. Note that this works +only for literals and not arbitrary type expressions. +For example, a constraint of the form KnownNat (a + b) +will not be simplified to +(KnownNat a, KnownNat b); instead, GHC will keep the +constraint as is, until it can simplify a + b to +a constant value. + + + + +It is also possible to convert a run-time integer or string value to +the corresponding type-level literal. Of course, the resulting type +literal will be unknown at compile-time, so it is hidden in an existential +type. The conversion may be performed using someNatVal +for integers and someSymbolVal for strings: -type family UnEx (k :: BOX) (ex :: Ex) :: k -type instance UnEx k (MkEx k x) = x +someNatVal :: Integer -> Maybe SomeNat +SomeNat :: KnownNat n => Proxy n -> SomeNat -Thus, the instance triggers only when the implicit parameter to UnEx -matches the implicit parameter to MkEx. Because k -is actually a parameter to UnEx, the kind is not escaping the -existential, and the above code is valid. +The operations on strings are similar. + +Computing With Type-Level Naturals -See also Trac #7347. +GHC 7.8 can evaluate arithmetic expressions involving type-level natural +numbers. Such expressions may be constructed using the type-families +(+), (*), (^) for addition, multiplication, +and exponentiation. Numbers may be compared using (<=?), +which returns a promoted boolean value, or (<=), which +compares numbers as a constraint. For example: + +GHC.TypeLits> natVal (Proxy :: Proxy (2 + 3)) +5 + + + +At present, GHC is quite limited in its reasoning about arithmetic: +it will only evalute the arithmetic type functions and compare the results--- +in the same way that it does for any other type function. In particular, +it does not know more general facts about arithmetic, such as the commutativity +and associativity of (+), for example. - - -Promoting type operators -Type operators are not promoted to the kind level. Why not? Because -* is a kind, parsed the way identifiers are. Thus, if a programmer -tried to write Either * Bool, would it be Either -applied to * and Bool? Or would it be -* applied to Either and Bool. -To avoid this quagmire, we simply forbid promoting type operators to the kind level. +However, it is possible to perform a bit of "backwards" evaluation. +For example, here is how we could get GHC to compute arbitrary logarithms +at the type level: + +lg :: Proxy base -> Proxy (base ^ pow) -> Proxy pow +lg _ _ = Proxy + +GHC.TypeLits> natVal (lg (Proxy :: Proxy 2) (Proxy :: Proxy 8)) +3 + -- cgit v1.2.1