Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Haskell - Illegal Polymorphic type?

Tags:

haskell

Why does the single usage of this type compile, but putting it into a list fails?

ft1  :: (Foldable t, Num a) => t a -> a
ft1   =   (F.foldl (+)  0)

fTest :: [(Foldable t, Num a) => t a -> a ]
fTest = [ F.foldl (+)  0 ]

The latter gives the error:

folding.hs:80:10:
    Illegal polymorphic or qualified type:
      (Foldable t, Num a) => t a -> a
    Perhaps you intended to use ImpredicativeTypes
    In the type signature for `fTest':
      fTest :: [(Foldable t, Num a) => t a -> a]

Simliarly, trying to name it fails (differently):

type Ftst t a = (Foldable t, Num a) => t a -> a

folding.hs:80:1:
    Illegal polymorphic or qualified type:
      (Foldable t, Num a) => t a -> a
    Perhaps you intended to use RankNTypes or Rank2Types
    In the type declaration for `Ftst'
like image 972
guthrie Avatar asked Jan 12 '15 04:01

guthrie


1 Answers

This restriction on Haskell's type system is in place to simplify type inference and checking. Type inference with predicative rank-1 types (see below) is decidable and has a relatively simple implementation. Type inference with rank-2 types is decidable but quite complicated, to the point that I don't know any language with an implementation of rank-2 type inference. Type inference for types of rank 3 and above is flat-out undecidable. Impredicative types also complicate things considerably; GHC used to have an implementation which allowed type-checking (and some very limited inference) with impredicative types, but it was so complicated that it was ripped out later. (Some values which only typecheck with impredicative types are still accepted by GHC at the moment, but I think this is not considered a "stable" feature.)

Quick definitions: rank-1 types have all quantification and class constraints "outside" the type, so all rank-1 types are of the form

forall a_1 ... a_m. (C_1, ..., C_n) => t

Rank-2 types allow function arguments to have rank-1 types; and in general rank n types allow function arguments to have rank (n-1) types.

Predicativity answers the question of what types can be substituted for type variables. If only monomorphic types (though potentially with type variables!) can be substituted, you are in a predicative system; impredicative types allow you to substitute a polymorphic type for a type variable. By extension, parametric data types in predicative systems can only accept monomorphic types as arguments. Thus, for example, your example which applies the [] type constructor to the type forall t a. (Foldable t, Num a) => t a -> a is trying to apply a constructor to a polymorphic type, hence is only valid in an impredicative system.

like image 142
Daniel Wagner Avatar answered Sep 30 '22 20:09

Daniel Wagner