Является ли «тип переменной» псевдоним «параметра типа»?

Question

Есть type variable и type parameter То же самое в Haskell? Например .:

ghci> :t last 
last :: [a] -> a 

a одновременно type variable и type parameter.

Answer 1

Вот сокращенный синтаксис для терминов типа уровня:

type ::= variable 
     | type type 
     | constructor 
     | "(" type ")" 

var ::= <lowercase letter>* 
constructor ::= <uppercase letter><lowercase letter>* 
       | "->" 
       | "[]" 

А вот сокращенный синтаксис для объявления новых типов данных:

decl  ::= "data" constructor var* "=" branches 
branches ::= branch | branch "|" branches 
branch ::= constructor type* 

Это не совсем точное или полное (см Report для канонических деталей), но этого достаточно, чтобы провести обсуждение с земли.

Вот поверхностное знание терминов и что я имею в виду, когда я говорю им:

• тип переменной: термин уровень типа, построенный var производства выше; например, a, , foo бы мелкие переменные типа, если они возникли в контексте ожидая типа, но [a], Tree, Ord x не переменные типа и не будет тип переменной в термине декларации f graph = undefined.
• тип параметр: a позиция в декларации данных, которая указывает на один из аргументов var; например, в data Foo a b c = Bar a Int Я бы назвал a, b и c слева от = параметров типа, но a справа не был бы. В меньшей степени «параметр типа» также используется для обозначения «аргумента типа», см. Ниже, хотя, на мой взгляд, это использование немного неряшливо.
• тип аргумент: тип заполнения для второй части type ::= type type производства выше; например, в Foo (Maybe a), я бы назвал a аргументом типа и (Maybe a) аргументом типа, но Foo и Maybe не был бы. В качестве специального случая у нас есть [a] в качестве своего рода синтаксического сахара для приложения [] a; в этом случае я бы также назвал a аргументом типа, хотя он был как бы забавным.

С этой терминологией в виде, в типе [a] -> a, я бы, конечно, назвать a переменного типа; Я бы возражал против вызова параметра типа a; и я был бы в порядке с вызовом a аргумента типа (поскольку он используется в приложении типа [] a, написанном в сладком стиле).

Обратите внимание, что даже если в этом случае можно было бы разумно назвать a как переменную типа и аргумент типа это не означает, что эти два термина являются синонимами!Сказать, что a - это переменная типа, указывает, что она еще не была сделана конкретной, тогда как утверждение, что a является аргументом типа, указывает на то, что оно используется для заполнения параметра другого типа, что подчеркивает два очень разные вещи о a в этом типе!

Просто округлить некоторые ответы с некоторыми примерами, демонстрирующих разницу между терминами, рассмотреть эти объявления типа, взятые из Prelude:

undefined :: a 
(>>=) :: Monad m => m a -> (a -> m b) -> m b 
not :: Bool -> Bool 
otherwise :: Bool 

a в типе undefined является переменным типом, но не аргумент типа; Аналогично, m в типе (>>=) является переменной типа, но в большинстве мест он не является аргументом типа.

Оба вида Bool в виде not являются аргументами типа, но не переменными типа. (Так же, как тип [t] сахар для [] t, тип t1 -> t2 сахар для (->) t1 t2.)

a и b в типе (>>=) являются переменными типа и типа аргументов.

Bool в типе otherwise не является ни переменной типа, ни аргументом типа.