Parameterized Types in Haskell

It would probably clear things up to use GADT notation, since the standard notation kind of mangles together the type- and value-level languages.

The standard Maybe type looks thus as a GADT:

{-# LANGUAGE GADTs #-}

data Maybe a where
  Nothing :: Maybe a
  Just :: a -> Maybe a

The “un-parameterised” version is also possible:

data EMaybe where
  ENothing :: EMaybe
  EJust :: a -> EMaybe

(as Joseph Sible commented, this is called an existential type). And now you can define

foo :: Maybe Int
foo = Just 37

foo' :: EMaybe
foo' = EJust 37

Great, so why don't we just use EMaybe always?

Well, the problem is when you want to use such a value. With Maybe it's fine, you have full control of the contained type:

bhrar :: Maybe Int -> String
bhrar Nothing = "No number "
bhrar (Just i)
 | i<0        = "Negative "
 | otherwise  = replicate i ''

But what can you do with a value of type EMaybe? Not much, it turns out, because EJust contains a value of some unknown type. So whatever you try to use the value for, will be a type error, because the compiler has no way to confirm it's actually the right type.

bhrar :: EMaybe -> String
bhrar' (EJust i) = replicate i ''
  =====> Error couldn't match expected type Int with a

If a variable is not reflected in the return type it is considered existential. This is possible to define data ExMaybe = ExNothing | forall a. ExJust a but the argument to ExJust is completely useless. ExJust True and ExJust () both have type ExMaybe and are indistinguisable from the type system's perspective.

Here is the GADT syntax for both the original Maybe and the existential ExMaybe

{-# Language GADTs                    #-}
{-# Language LambdaCase               #-}
{-# Language PolyKinds                #-}
{-# Language ScopedTypeVariables      #-}
{-# Language StandaloneKindSignatures #-}
{-# Language TypeApplications         #-}

import Data.Kind (Type)
import Prelude hiding (Maybe(..))

type Maybe :: Type -> Type
data Maybe a where
  Nothing ::      Maybe a
  Just    :: a -> Maybe a

type ExMaybe :: Type
data ExMaybe where
  ExNothing ::      ExMaybe
  ExJust    :: a -> ExMaybe

You're question is like asking why a function f x = .. needs to specify its argument, there is the option of making the type argument invisible but this is very odd but the argument is still there even if invisible.

-- >> :t JUST
-- JUST :: a -> MAYBE
-- >> :t JUST 'a'
-- JUST 'a' :: MAYBE
type MAYBE :: forall (a :: Type). Type
data MAYBE where
  NOTHING ::      MAYBE @a
  JUST    :: a -> MAYBE @a

mAYBE :: b -> (a -> b) -> MAYBE @a -> b
mAYBE nOTHING jUST = \case
  NOTHING -> nOTHING
  JUST a  -> jUST a

Having explicit type parameters makes it much more expressive. You lose so much information without it. For example, how would you write the type of map? Or functors in general?

map :: (a -> b) -> [a] -> [b]

This version says almost nothing about what’s going on

map :: (a -> b) -> [] -> []

Or even worse, head:

head ::  [] -> a

Now we suddenly have access to unsafe coerce and zero type safety at all.

unsafeCoerce :: a -> b
unsafeCoerce x = head [x]

But we don’t just lose safety, we also lose the ability to do some things. For example if we want to read something into a list or Maybe, we can no longer specify what kind of list we want.

read :: Read a => a

example :: [Int] -> String

main = do
  xs <- getLine
  putStringLine (example xs)

This program would be impossible to write without lists having an explicit type parameter. (Or rather, read would be unable to have different implementations for different list types, since content type is now opaque)

It is however, as was mentioned by others, still possible to define a similar type by using the ExistentialQuantification extension. But in those cases you are very limited in how you can use those data types, since you cannot know what they contain.