Почему мы не можем сопоставить шаблон с Set / Type в Coq / Agda / Idris？ - PullRequest
Новая
       33

Почему мы не можем сопоставить шаблон с Set / Type в Coq / Agda / Idris？

0 голосов
/ 08 сентября 2018

Подумайте о функции, которая принимает Set и возвращает длину в байтах с именем byteLength: 

byteLength : Set -> Maybe Nat

и если я хочу реализовать эту функцию напрямую, мне нужно сопоставить шаблон с аргументом типа: 

byteLength Char = Just 1
byteLength Double = Just 8
byteLength _ = Nothing

, но приведенный выше код не компилируется, так как сопоставление с образцом в Set / Type не разрешено.

поэтому мы должны определить интерфейс как обходной путь 

Interface ByteLength a where
    byteLength : Nat

implement ByteLength Char where
    byteLength = 1

и в более общем смысле, может быть, мы можем использовать что-то вроде TypeRep, чтобы выполнить аналогичное сопоставление с образцом в TypeRep. но TypeRep также определяется как интерфейс.

Я думаю, что использование Interface и использование forall очень разные, поскольку Interface означает «для некоторых типов», а forall означает «для всех типов».

Мне интересно, почему эти языки DT не поддерживают сопоставление с образцом в Set / Type, есть ли какая-то особая причина, которую я не знаю?

1 Ответ

0 голосов
/ 08 сентября 2018

В Agda, Idris, Haskell и многих других языках квантификация по типам составляет параметрический (в отличие от специального полиморфизма , где вам разрешено сопоставлять типы). С точки зрения реализации это означает, что компилятор может стереть все типы из программы, поскольку функции никогда не могут в вычислительном отношении зависеть от аргумента типа Set. Возможность стереть типы особенно важна для языков с зависимой типизацией, поскольку типы часто могут превращаться в огромные выражения.

С более теоретической точки зрения параметрический полиморфизм хорош, потому что он позволяет нам вывести определенные свойства функции, просто взглянув на ее тип, красноречиво описанный как "свободные теоремы" Фила Уодлера . Я мог бы попытаться дать вам суть статьи, но вы должны просто пойти и прочитать ее вместо этого.

Конечно, иногда для реализации функции требуется специальный полиморфизм, поэтому у Haskell и Idris есть классы типов (Agda имеет аналогичную функцию, называемую аргументы экземпляра , и Coq имеет канонические структуры , а также классы типов). Например, в Agda вы можете определить запись следующим образом: 

record ByteLength (A : Set) : Set where
  field
    theByteLength : Nat
open ByteLength

byteLength : (A : Set) {{_ : ByteLength A}} -> Nat
byteLength A {{bl}} = bl .theByteLength

и затем вы можете определить функцию byteLength для различных типов, определив экземпляры: 

instance
  byteLengthChar : ByteLength Char
  byteLengthChar .theByteLength = 1

  byteLengthDouble : ByteLength Double
  byteLengthDouble .theByteLength = 8

С этим кодом byteLength Char оценивается в 1, а byteLength Double оценивается в 8, в то время как это вызовет ошибку типа для любого другого типа.

...