为什么`Just String`在Haskell中会出错

Question

嗨我在学习Haskell中的参数化类型主题时遇到了一个微不足道但令人筋疲力尽的问题.这是我的问题:

看这是定义Maybe:

data Maybe a = Just a | Nothing

我们使用这个:

Just "hello world"
Just 100

但为什么不能只采取一个类型变量？

例如:

Just String
Just Int

我知道这个问题很傻,但我还是想不出来......

Answer 1

好吧,首先要注意String并且Int不是类型变量,而是类型(类型常量,如果你愿意的话).但这对你的问题的目的并不重要.

重要的是Haskells 类型语言和价值语言之间的命运.这些通常是分开的.String并Int与Maybe住在型语言,而"hello world"与100和Just和Nothing住在价值的语言.每个人都对另一方一无所知.只有,编译器知道"这种值的描述属于该类型",但实际类型仅在编译时存在,并且值仅在运行时存在.

有两件事令人困惑:

• 允许使用类型和值语言存在的名称.最知名的是()和同义词类似

  newtype Endo a = Endo { runEndo :: a -> a }
  

  但实际上这些是两个单独的实体:类型构造函数Endo :: *->*(参见下面的这些*内容)和值构造函数Endo :: (a->a) -> Endo a.它们只是碰巧共享相同的名称,但是在完全不同的范围内 - 就像你声明两者一样,addTwo x = x + 2并且greet x = "Hello "++x在x符号的两个使用都与彼此无关的情况下.

• 该data语法似乎交融类型和值.在其他任何地方,类型和值必须始终用a分隔::,最常见的是签名

       "hello world" :: String
       100           :: Int
       Just          :: Int -> Maybe Int
          {-hence-}Just 100 :: Maybe Int
       Nothing       :: Maybe Int
  
  foo :: (Num a, Ord a) => a -> Maybe a  -- this really means `forall a . (Num a, Ord a) => a -> Maybe a
  foo n | n <= 0     = Nothing
        | otherwise  = Just $ n - 1
  

  事实上data,如果启用,语法也可用于以更独特的方式定义-XGADTs:

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

  现在我们::再次明确区分值级(左)和类型级.

你实际上可以把它提升一个级别:也可以写上面的声明

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

这里Maybe :: * -> *的意思是" Maybe是一个类型级的事情样 * -> * ",即它需要类型的类型级参数*(如Int)和返回类型的另一种类型的层次的东西*(在这里Maybe Int).类型与类型相关的类型.