wiki:TypeNats/ImplicitExplicit

Version 2 (modified by diatchki, 3 years ago) (diff)

--

There are two different styles of writing functions which need the integer corresponding to a type level natural.

The one approach is to use an explicit parameter of type Nat n. For example:

memset :: Storable a => ArrPtr n a -> a -> Nat n -> IO ()
memset = ...

This style is, basically, a more typed version of what is found in many standard C libraries. Callers of this function have to pass the size of the array explicitly, and the type system checks that the size matches that of the array. When defining memset we can just use natToInteger on the Nat n parameter to get the actual value of the array size.

The other approach is to use an implicit parameter by using the class TypeNat. For example:

memsetAuto :: (Storable a, TypeNat n) => ArrPtr n a -> a -> IO ()

In this style, the caller of the function does not need to provide the type of the array explicitly. Instead, it is computed automatically from the type of the array. When defining memsetAuto we can use nat, the method of TypeNat, to get access to the value corresponding to the type level natural.

When using the implicit style, it is important that the type of nat is specified precisely. Failing to do so typically results in ambiguity errors (i.e., GHC does not know which integer it should use). Another common mistake is to forget that 'nat' is a polymorphic value and so every time it is used it may refer to a different value.

An easy way to avoid such problems is to implement the implicit style functions in terms of the explicit ones. For example, we can implement memsetAuto like this:

memsetAuto arr val = memset arr val nat