Понимание сигнатуры типа данных, класса типов и превращения типа данных в экземпляр класса типов

Читал Learn You A Haskell For a Great Good! и есть большие проблемы с пониманием экземпляра и рода.

Q1: Значит, тип t в Tofu t действует как функция с доброй сигнатурой (* -> (* -> *)) -> *? И общий добрый знак tofu - * -> *, не так ли? поскольку (* -> *) -> * приводит к * и (* -> (* -> *)) -> * тоже

Q2: Когда мы хотим создать Frank a b экземпляр класса типов Tofu t, тип данных Frank a b также должен иметь тот же тип с t. Это означает, что вид a это *, b * -> * и b a, который будет (* -> *) -> *, что приводит к *. Это верно?

Q3: x в tofu x представляет j a, поскольку оба имеют вид *. Frank с его видом (* -> (* -> *)) -> * применяется на x. Но я не уверен, как представление j a как x будет различать x в tofu x, который равен j a, и x в Frank x, который равен a j.

Я как бы новичок в идее наличия функции внутри типа или класса данных (например: b в Frank a b или t в Tofu t), что немного сбивает с толку

Я оставляю ссылку здесь, поскольку цитирование сделает сообщение излишне длинным. ссылка

class Tofu t where
  tofu :: j a -> t a j

data Frank a b = Frank {frankField :: b a} 

instance Tofu Frank where
  tofu x = Frank x

typeclass haskell type-kinds
person Jung    schedule 11.02.2019    source источник
comment
Это действительный код? Мне нужно включить какие-то расширения? Все, что я получаю, это сообщения об отказе от компиляции. В частности, в уравнении instance Tofu Frank отсутствует привязка LHS для t или b. Откуда они берутся?   -  person AntC    schedule 11.02.2019
comment
Помимо :kind, который показывает LYAH, есть также :info, который сообщает вам все, что GHC знает о ваших именах. Например, :i Tofu сообщает предполагаемый вид для t; :i Frank сообщает вам предполагаемые виды для a, b.   -  person AntC    schedule 11.02.2019
comment
@AntC Мне очень жаль, что код instance был неправильным. Я исправил это.   -  person Jung    schedule 11.02.2019
comment
Благодарю. Я нашел поучительный момент, пытаясь добиться результата от применения tofu. (Добавьте deriving Show в объявление данных для Frank.) Запись tofu (Just "hello") дает неприятные ошибки типа.   -  person AntC    schedule 11.02.2019

Ответы (2)


arrow_upward
6
arrow_downward

Q1:

Итак, тип t в Tofu t действует как функция с сигнатурой вида (* -> (* -> *)) -> *?

t имеет вид * -> (* -> *) -> *, точнее * -> ((* -> *) -> *), а не (* -> (* -> *)) -> *.

И общий добрый знак тофу - * -> *, не так ли?

tofu не имеет доброй подписи, только конструкторы типов; его тип вид *. Таковы его типы аргументов и результатов. И то же самое для любой функции.

Q2: Вы начинаете с неверного предположения: instance Tofu Frank делает конструктор типа Frank экземпляром Tofu, а не Frank a b. Итак, это Frank, который должен иметь тот же вид, что и t, а не Frank a b (который имеет вид *).

b a, который будет (* -> *) -> *

Нет, b a - это приложение типа b вида * -> * до a вида *, поэтому приложение имеет вид *. Точно так же, как если бы b был функцией типа x -> y, а a был значением типа x, b a имел бы тип y, а не (x -> y) -> x: просто замените x и y на *.

Q3:

X в тофу x обозначает j a

«Имеет тип», а не «представляет».

так как оба имеют вид *

x не имеет вида, потому что это не тип.

Франк с его видом (* -> (* -> *)) -> * применяется к x

No, in

tofu x = Frank x

это Frank конструктор данных, который применяется к x, а не конструктор типа . Это функция с подписью b a1 -> Frank a1 b (переименование a, чтобы не путать с tofu). Итак, b ~ j и a1 ~ a.

person Alexey Romanov    schedule 11.02.2019

arrow_upward
3
arrow_downward

Алексей уже попытался ответить на ваши вопросы. Вместо этого я объясню ваш пример с любыми подробностями, которые кажутся важными.

class Tofu t where
  tofu :: j a -> t a j
          ^^^    ^^^^^
          ^^^^^^^^^^^^

Выделенные биты должны иметь вид *. Все, что находится по обе стороны от стрелки (уровня типа), должно иметь тип * [1], а сам термин стрелки (то есть весь термин j a -> t a j) также имеет тип *. В самом деле, любой "тип" [2], который может содержать значение, имеет вид *. Если у него есть какой-либо другой вид, у него не может быть никаких значений (он просто используется для создания правильных типов в другом месте).

Итак, в подписи tofu выполняется следующее:

j a :: *
t a j :: *

потому что они используются как «обитаемые» типы, поскольку являются аргументами для (->).

И это единственное, что сдерживает класс. В частности, a может быть любым. С PolyKinds [3]

a :: k   -- for any kind k
j :: k -> *
t :: k     ->   (k -> *) -> *
     ^          ^^^^^^^^    ^
 kind of a      kind of j   required since is used as inhabited type by ->

Итак, мы нашли нужный вид t.

Мы можем использовать аналогичные рассуждения для Frank.

data Frank a b = Frank {frankField :: b a}
     ^^^^^^^^^                        ^^^

Снова выделенные биты должны иметь вид *, потому что они могут иметь значения. В остальном ограничений нет. Обобщая, имеем

a :: k
b :: k -> *
Frank a b :: *

И поэтому

Frank :: k -> (k -> *) -> *

Мы видим, что вид Frank соответствует требуемому виду для Tofu. Но это также имеет смысл для более конкретного вида, например:

data KatyPerry a b = KatyPerry a (b Int)

Попробуйте определить ее вид и убедитесь, что он более конкретен, чем тот, который требуется Tofu.

[1] Это верно даже для стрелок на уровне доброты, если мы предположим TypeInType. Без TypeInType «виды типов» называются сортами, и никто о них не заботится; на этом уровне обычно не происходит ничего интересного.

[2] Я заключил «тип» в кавычки, потому что технически только вещи с типом * называются типами, все остальное называется конструктором типов. Я попытался уточнить это, но не смог найти удобного способа сослаться на оба сразу, и абзац получился очень беспорядочным. Так что «тип».

[3] Без PolyKinds все, что имеет неограниченный вид, например k, специализируется на *. Это также означает, что тип Tofu может зависеть от того, какой тип вы впервые создаете для него, или от того, создаете ли вы его для типа в том же модуле или в другом модуле. Это плохо. PolyKinds это хорошо.

person luqui    schedule 11.02.2019
comment
Я считаю ваш ответ очень полезным и конструктивным, как всегда. 2 вопроса: это правильно b a :: (* -> *) -> * -> *? Это правильный ответ на домашнее задание? a (b Int) :: * -> (Int -> *) -> * ;a :: k ;b :: Int -> * ;KatyPerry :: * -> (Int -> *) -> * - person Jung; 11.02.2019
comment
извините, я не могу обойтись с разрывом строки внутри кода, поэтому его трудно читать. Тоже одно. Я вижу, вы выделяете Frank a b, но не Frank в правой части =. Почему это так? Это как-то связано с синтаксисом записи? - person Jung; 11.02.2019