Как я могу продемонстрировать, что этот тип будет выведен? - PullRequest
Новая
       46

Как я могу продемонстрировать, что этот тип будет выведен?

0 голосов
/ 17 мая 2018

Я перехожу, вывод типа Хаскеля немного сложен для меня, хотя кажется, что это просто.

С учетом этой функции: nat x = x : ( nat (x+1))

типа: Num t => t -> [t]

и это понятно, потому что функция nat берет элемент и создает бесконечный список.

Но теперь меня просят указать тип head (nat 2)

Я полностью понимаю, почему и какой тип head :: [a] -> a

Но почему head (nat 2) :: Num c => c кто-то может объяснить, почему?

Начиная с самого общего типа, который является A -> B (я предполагаю, что это A -> B, потому что он принимает один аргумент) Что дальше?

РЕДАКТИРОВАТЬ

Это Give the type of the expression: head (nat 2) означает, что я должен указать тип функции или просто просто возвращаемое значение, которое на самом деле должно быть числом, и именно поэтому это Num c => c, я только что ответил на свой вопрос?

Оригинальный вопрос: Give the type of the expression: head (nat 2)

Обоснуйте свой ответ.

Спасибо

1 Ответ

0 голосов
/ 17 мая 2018

Хорошо, давайте предположим, что мы уже получили тип nat, и мы знаем тип head :: [a] -> a

nat :: Num a => a -> [a]
head :: [b] -> b

Затем мы используемИмена переменных другого типа a и b, так как в настоящее время мы ничего не знаем о a и b, и, следовательно, мы предполагаем, что может быть разными, и, следовательно, назначаем другоеname.

Теперь мы видим (nat 2) в выражении.Мы знаем, что 2 имеет тип: 

2 :: Num c => c

Так что это означает, что nat 2 имеет тип: 

nat     :: Num a => a -> [a]
2       :: Num c => c
----------------------------
(nat 2) :: Num a =>      [a]

, и мы знаем, что a ~ c (a и c того же типа).Мы знаем это, поскольку 2 является параметром вызова функции с nat в качестве функции, а nat имеет тип параметра a.Следовательно, тип 2 и параметр nat должны быть одинаковыми.

Теперь мы вызываем head с аргументом (nat 2), так что это означает, что мы рассуждаем так: 

head         ::          [b] -> b
(nat 2)      :: Num a => [a]
---------------------------------
head (nat 2) :: Num b =>        b

И мы знаем, что a ~ b, поскольку тип nat 2 равен [a], а первый параметр head должен иметь тип [b].Таким образом, это означает, что, начиная с a ~ b, это означает, что ограничение типа Num a также означает Num b, и наоборот.

Итак, тип: 

head (nat 2) :: Num b => b
...