Возможно совпадение совпадений функций на уровне типа, но не на уровне значений, почему это различие?

Question

В this работе SPJ, на странице 3 и 4, написано:

class Mutation m where 
    type Ref m :: * -> * 
    newRef :: a -> m (Ref m a) 
    readRef :: Ref m a -> m a 
    writeRef :: Ref m a -> a -> m() 

instance Mutation IO where 
    type Ref IO = IORef 
    newRef = newIORef 
    readRef = readIORef 
    writeRef = writeIORef 

instance Mutation (ST s) where 
    type Ref (ST s) = STRef s 
    newRef = newSTRef 
    readRef = readSTRef 
    writeRef = writeSTRef 

и:

Объявление класса в настоящее время представляет тип функции Ref (с указанного вида) наряду с обычные функции значений, такие как newRef (каждый с указанным типом). Аналогично, каждое объявление экземпляра вносит предложение, определяющее функцию типа в типе экземпляра , рядом с свидетелем для каждой функции значения.

Мы говорим, что Ref является типом семейства или связанным типом класса Mutation. Он ведет себя как функция на уровне уровня, поэтому мы также вызываем Ref функцию типа. Применение функции типа использует тот же синтаксис, что и применение конструктора типа : Ref m a выше означает применить функцию типа Ref to m, , затем применить полученный конструктор типа к a.

То есть, другими словами,

Ref :: (*->*)->*->*

, который, Ref принимает функцию уровня типа в качестве аргумента, как Maybe или IO или [] и производит другую функцию уровня типа, такие, как IORef использованием a соответствие шаблону, т.е. Ref определяется знаком .

Итак, как возможно, что можно сопоставлять шаблоны с функциями на уровне типа, но не на уровне значений?

Например,

fun2int:: (Int->Int)->Int 
fun2int (+)=2 
fun2int (*)=3 

не возможно писать, потому что равенство на функциях является undecidable.

1) Так как же возможно, что на уровне типа это не вызывает проблем?

2) Это потому, что функции на уровне типа имеют очень ограниченный вид? Таким образом, никакая функция на уровне уровня не может быть аргументом Ref, только несколько выбранных, а именно те, которые объявлены программистом, а не такие функции, как (+), которые являются более общими, чем те, которые были объявлены программистом? Является ли это причиной того, что при сопоставлении шаблонов функций уровня типа нет проблем?

3) Является ли ответ на этот вопрос связанным с this частью спецификации GHC?

Answer 1

Коротко говоря, нет никакого сопоставления с образцом на функции типа уровня значения, но только на их имени.

В Haskell, как и во многих других языках, типы хранятся отдельно от их имени, даже если их представление идентично.

data A x = A Int x 
data B x = B Int x 

Выше, A и B два различных типа конструктора, даже если они описывают ту же самую функцию типа уровня: в псевдокоде \x -> (Int, x), примерно. В некотором смысле эти две идентичные функции уровня имеют другое имя/идентификатор.

Это отличается от

type C x = (Int, x) 
type D x = (Int, x) 

которые оба описывают ту же функцию типа уровня, как указано выше, но не вводить два новых имен типов. Вышеизложенное является лишь синонимами: они обозначают функцию, но не имеют своей собственной идентичности.

Поэтому можно добавить экземпляр класса для A x или B x, но не для C x или D x: попытка сделать последнее будет добавить экземпляр типа (Int, x) вместо этого, связывающего экземпляра с именами типа (,), Int вместо.

На уровне ценности ситуация не так сильно отличается. В самом деле, там есть конструкторы значений, которые являются специальными функциями с именем/идентификатором и регулярными функциями без фактического тождества. Мы можем шаблон матч против шаблона, построенного из конструкторов, но не против что-нибудь еще

case expOfTypeA of A n t -> ... -- ok 
case someFunction of succ -> ... -- no 

Обратите внимание, что на уровне типа мы не можем сделать по шаблону, который легко. Haskell позволяет делать это только с использованием классов типов. Это делается для сохранения некоторых теоретических свойств (параметричности), а также для эффективной реализации (разрешая стирание типа - мы не должны пометить каждое значение своим типом во время выполнения). Эти функции выходят за рамки ограничения соответствия шаблону типа на классы классов - это накладывает определенную нагрузку на программиста, но преимущества перевешивают недостатки.

Answer 2

{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds #-} 
import GHC.TypeLits 

Давайте нарисуем несколько параллелей между типом и значением уровня в Haskell.

Первый, у нас есть неограниченные функции как по типу, так и по значению. На уровне типа вы можете выражать почти все, используя семейства типов. Вы не могут соответствие шаблону произвольным функциям на любом типе или уровне значения. Например. Вы не можете сказать,

type family F (a :: *) :: * 
type family IsF (f :: * -> *) :: Bool where 
    IsF F = True 
    IsF notF = False 

-- Illegal type synonym family application in instance: F 
-- In the equations for closed type family ‘IsF’ 
-- In the type family declaration for ‘IsF’ 

Второй, мы полностью примененные данные и конструкторы типов, такие как Just 5 :: Maybe Integer на ценностном уровне или Just 5 :: Maybe Nat на уровне типа.

Можно шаблон матча на них:

isJust5 :: Maybe Integer -> Bool 
isJust5 (Just 5) = True 
isJust5 _ = False 

type family IsJust5 (x :: Maybe Nat) :: Bool where 
    IsJust5 (Just 5) = True 
    IsJust5 x = False 

Обратите внимание на разницу между произвольными функциями и типом данных/конструкторы. Свойство конструкторов иногда называют Generativity. Для двух различных функций f и g, вполне возможно, что f x = g x для некоторых x. С другой стороны, для конструкторов f x = g x подразумевает f = g.Это отличие делает первый случай (сопоставление шаблонов на произвольных функциях) неразрешимым, а второй случай (сопоставление шаблонов на полностью применимых конструкторах) разрешимым и доступным.

До сих пор мы видели согласованность по типу и уровню ценности.

И наконец,, мы частично применили (включая не применяемые) конструкторы. На типовом уровне они включают Maybe, IO и [] (непримененный), а также Either String и (,) Int (частично применяется). На уровне значения мы не применяем Just и Left, а частично применяем (,) 5 и (:) True.

Условие генеративности не имеет значения, заполнено или нет приложение; поэтому нет ничего исключающего совпадения шаблонов для частично применяемых конструкторов. Это то, что вы видите на уровне типа; и может тоже иметь значение.

type family IsLeft (x :: k -> k1) :: Bool where 
    IsLeft Left = True 
    IsLeft x = False 

isLeft :: (a -> Either a b) -> Bool 
isLeft Left = True 
isLeft _ = False 
-- Constructor ‘Left’ should have 1 argument, but has been given none 
-- In the pattern: Left 
-- In an equation for ‘isLeft’: isLeft Left = True 

Причина, по которой это не поддерживается, - это эффективность. Вычисления на уровне типа выполняются во время компиляции в интерпретируемом режиме; поэтому мы можем позволить переносить множество метаданных о типах и типах функций для соответствия шаблону по им.

Вычисления на уровне значения составлены и должны быть такими же быстрыми, как . Сохранение достаточного количества метаданных для поддержки сопоставления шаблонов частично с помощью прикладных конструкторов усложняло бы компилятор и замедляло бы программу на runtime; это слишком много, чтобы заплатить за такую ​​экзотическую особенность.