Takayuki Muranushi wrote:
> Today, I encountered a strange trouble with higher-rank polymorphism. It
> was finally solved by nominal typing. Was it a bug in type checker? lack of
> power in type inference?
> runDB :: Lens NetworkState RIB
> runDB = lens (f::NetworkState -> RIB) (\x s -> s { _runDB = x })
> where f :: NetworkState -> RIB
As it becomes apparent (eventually), RIB is a polymorhic type,
something like
type RIB = forall a. DB.DBMT (Maybe Int) IO a0
-> IO (StM (DB.DBMT (Maybe Int) IO) a0)
The field _runDB has this polymorphic type. Hence the argument x
in (\x s -> s { _runDB = x }) is supposed to have a polymorphic type.
But that can't be: absent a type signature, all arguments of a
function are monomorphic. One solution is to give lens explicit,
higher-ranked signature (with explicit forall, that is). A better
approach is to wrap polymorphic types like your did
> newtype RIB = RIB (RunInBase (DB.DBMT (Maybe Int) IO) IO)
The newtype RIB is monomorphic and hence first-class, it can be freely
passed around. In contrast, polymorphic values are not first-class,
in Haskell. There are many restrictions on their use. That is not a
bug in the type checker. You may call it lack of power in type
inference: in calculi with first-class polymorphism (such as System F
and System Fw), type inference is not decidable. Even type checking is
not decidable.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
