Why does the type of a function have to be "wrapped" for type checking?
The following program type checks:
{-# LANGUAGE RankNTypes #-}
import Numeric.AD (grad)
newtype Fun = Fun (forall a. Num a => [a] -> a)
test1 [u, v] = (v - (u * u * u))
test2 [u, v] = ((u * u) + (v * v) - 1)
main = print $ fmap (\(Fun f) -> grad f [1,1]) [Fun test1, Fun test2]
But this program doesn't work:
main = print $ fmap (\f -> grad f [1,1]) [test1, test2]
With a type error:
Grad.hs:13:33: error:
• Couldn't match type ‘Integer’
with ‘Numeric.AD.Internal.Reverse.Reverse s Integer’
Expected type: [Numeric.AD.Internal.Reverse.Reverse s Integer]
-> Numeric.AD.Internal.Reverse.Reverse s Integer
Actual type: [Integer] -> Integer
• In the first argument of ‘grad’, namely ‘f’
In the expression: grad f [1, 1]
In the first argument of ‘fmap’, namely ‘(\ f -> grad f [1, 1])’
Intuitively, the last program looks right. In the end, the following seemingly equivalent program actually works:
main = print $ [grad test1 [1,1], grad test2 [1,1]]
This is similar to a limitation in the GHC type system. I would like to know what is causing the failure, why this limitation exists, and any possible workarounds other than function wrapping (per Fun
above).
(Note: this is not caused by the monomorphism constraint; compiling with NoMonomorphismRestriction
does not help.)
source to share
This is a problem with a GHC type system. By the way, this is really a GHC type system; the original type system for Haskell / ML like languages does not support higher rank polymorphism, let alone the non-specific polymorphism we are using here.
The problem is that in order to type validation, we need to support forall
at any position in the type. Not only grouped along the entire front of the type (normal limitation that type inference allows). When you leave this area, type inference becomes generally undecidable (for rank n polymorphism onwards). In our case, the type [test1, test2]
must be [forall a. Num a => a -> a]
, which is a problem, given that it does not fit into the scheme described above. This will require us to use non-discriminatory polymorphism, so called because it a
covers the types with forall
in them and therefore a
can be replaced by the type in which it is used.
So, therefore, there will be some cases that erroneously refer to the fact that the problem is not completely solvable. GHC has some support for rank n polymorphism and some support for non-performing polymorphism, but it's usually best to just use newtype wrappers to get reliable behavior. As far as I know, the GHC also discourages using this function precisely because it is so difficult to determine what the type inference algorithm will handle.
So math says there will be inflectional cases, and newtype
wrappers are the best, if somewhat unsatisfactory, way to deal with it.
source to share
The type inference algorithm will not infer higher rank types (those forall
on the left of ->
). If I remember correctly, it becomes insoluble. Anyway, consider this code
foo f = (f True, f 'a')
What type should it be? We could have
foo :: (forall a. a -> a) -> (Bool, Char)
but we might as well have
foo :: (forall a. a -> Int) -> (Int, Int)
or, for any constructor like F :: * -> *
foo :: (forall a. a -> F a) -> (F Bool, F Char)
Here, as far as I can see, we cannot find the main type - the type, which is the most general type that we can assign foo
.
If the main type does not exist, the type inference engine can select only the suboptimal type for foo
, which can later cause type errors. This is bad. Instead, GHC uses the Hindley-Milner type inference mechanism, which has been extensively extended to cover the more advanced Haskell types. This mechanism, unlike plain Hindley-Milner, assigns a f
polymorphic type if the user explicitly requires it, eg. giving a foo
signature.
Using a new wrapper type such as Fun
also instructs GHC in a similar way by providing a polymorphic type for f
.
source to share