Почему мой шаблон блокирует ошибку с обеих сторон?

#haskell #pattern-matching #pattern-synonyms

Вопрос:

Чтобы начать все это, я работаю с синонимом шаблона, определенным следующим образом:

 {-# Language PatternSynonyms #-}

pattern x := y <- x @ y
 

Это позволяет мне запускать несколько совпадений шаблонов по одному параметру одновременно. Обычный as binding ( @ ) не позволяет левой стороне быть шаблоном, но это так.

С помощью этого я создаю следующую игрушечную функцию

 {-# Language ViewPatterns #-}
f ((_:_) := (head -> y)) =
  [ y ]
f [] =
  []
 

Я уверен, что это не лучший способ реализовать это, но это минимальный рабочий пример для рассматриваемого поведения.

У этого есть функция, которая принимает один параметр. Он сопоставляет параметр с двумя шаблонами, используя определенный синоним. Первый шаблон соответствует любому непустому списку и не содержит привязок. Второй запускает функцию head в списке и привязывается y к результату.

Таким образом, вопрос в том, может head ли это вызвать ошибку или другой шаблон предотвратит ее?

 >>> f []
[]
 

Другой шаблон предотвращает это! Хорошо, значит, если я сделаю их в другом порядке, то это должно сломаться, верно?

 f' ((head -> y) := (_:_)) =
  [ y ]
f' [] =
  []
 
 >>> f' []
[]
 

Нет! Это все еще работает. Итак, теперь мой вопрос: делает ли второй шаблон вообще что-нибудь? Возможно, шаблоны просмотра имеют какое-то разумное поведение, когда он вызывает функцию и завершает работу шаблона, если возникает ошибка …

 f'' (head -> y) =
  [ y ]
f'' [] =
  []
 
 >>> f'' []
[*** Exception: Prelude.head: empty list
 

Нет… это не. Это не удается. Каким-то образом (_:_) блокирует ошибку, независимо от того, на какой стороне она находится. Может быть, ghc предпочитает сопоставлять шаблоны деструктурирования перед шаблонами просмотра? Чтобы проверить это, я могу заменить шаблон (_:_) на (reverse -> _:_) . Таким образом, он должен запустить функцию, прежде чем сможет приступить к деструктуризации.

Но, протестировав его, новый паттерн не меняет поведения. Эту гипотезу можно исключить.

Так, может быть, это лень? x невозможно оценить, если список пуст, поэтому он находится в состоянии ожидания, и ошибка никогда не возникает. Похоже, в какой-то степени это так и есть. Если я заменю (head -> x) на «у (undefined -> x) нас не изменится поведение».

Однако, если я заменю его на (undefined -> "yo") :

 f ((undefined -> "yo") := (x:_)) = [x]
f [] = []
 
 >>> f []
*** Exception: Prelude.undefined
 

Это undefined действительно оценивается. Что, по-видимому, указывает на то, что шаблон вынуждает оценку сравнивать "yo" . И если я сейчас поменяю порядок:

 f ((x:_) := (undefined -> "yo")) = [x]
f [] = []
 
 >>> f []
[]
 

Это не оценивается. Похоже, что сейчас мы замыкаем совпадение с шаблоном.

Значит, гипотеза о лени, по-видимому, имеет смысл? Это все еще очень непрозрачно для меня, и я хотел бы, чтобы кто-то с большим опытом работы с внутренними функциями ghc подтвердил эту гипотезу.

Итак, мой вопрос теперь в том, что происходит? Может быть, это лень? Как это работает?

Большое спасибо пользователю discord Лекси. До сих пор они очень помогали в диагностике.

Комментарии:

1. Что ж, это интересно. Но… мы действительно хотим туда поехать ? PatternSynomyms и так является одним из наиболее сомнительных расширений; я бы не стал использовать его для шаблонов, которые делают намного больше, чем когда-либо должны были делать шаблоны.

Ответ №1:

Вы действительно наблюдаете эффект лени.

Давайте начнем с гораздо более простого примера:

 f :: () -> Int
f x = 42
 

Лень f undefined возвращается 42 . Это связано с тем, что шаблон переменной x не требует вычисления аргумента, поэтому undefined он никогда не требуется.

Для сравнения, если бы мы использовали

 f :: () -> Int
f () = 42
 

затем f undefined происходит сбой, так как шаблон () требует, чтобы аргумент оценивался до тех пор, пока он не откроет () конструктор (что в данном случае означает полную оценку).

Аналогично,

 f :: String -> Int
f x = 42
 

заставит f undefined вернуться 42 , в то время как

 f :: String -> Int
f (x:xs) = 42
 

приведет f undefined к сбою, после попытки оценить undefined , чтобы открыть первый конструктор списка (или : или [] ).

У нас также есть это

 f :: String -> Int
f "yo" = 42
f x    = 0
 

делает f undefined сбой: ведь шаблон "yo" означает ('y':'o':[]) , что он будет заставлять undefined , пытаясь сопоставить его с первым : . Более подробно, все следующие вызовы завершатся сбоем:

 f undefined
f (undefined:anything)
f ('y':undefined)
f ('y':undefined:anything)
f ('y':'o':undefined)
 

Здесь anything может быть undefined или любая другая строка/символ по мере необходимости.

Для сравнения, все следующие вызовы будут возвращены 0 , так как первый шаблон в определении не соответствует (без сбоя!):

 f []
f ('a':anything)
f ('y':'a':anything)
f ('y':'o':anything:anything)
 

Опять же, anything может быть undefined или любая другая строка/символ по мере необходимости.

Это связано с тем, что сопоставление шаблонов "yo" выполняется примерно так:

  • оценивайте входное значение x до тех пор, пока WHNF (не откроет свой первый конструктор)
    • если это так [] , потерпите неудачу
    • если это так y:ys , оцените y до WHNF
      • если y есть другой символ, чем 'y' , потерпите неудачу
      • если y 'y' да , то оценивайте ys до WHNF
        • если это » []», потерпите неудачу
        • если это так z:zs , оцените z до WHNF
          • если z есть другой символ, чем 'o' , потерпите неудачу
          • если z 'o' да , то оценивайте zs до WHNF
            • если это так [] , добейтесь успеха!!
            • если это так h:hs , потерпите неудачу

Обратите внимание, что в каждой «оценке .. до» точки WHNF » мы могли бы потерпеть крах (или застрять в бесконечном вычислении) из-за днищ.

По сути, сопоставление с шаблоном выполняется слева направо и останавливается, оценивая входные данные ровно столько, сколько необходимо, и останавливаясь, как только становится известен результат (сбой/успех). Это не обязательно приведет к полной оценке входных данных. При сбое мы даже не обязательно оцениваем входные данные так глубоко, как шаблон, если обнаруживаем раннюю точку сбоя. Это действительно то, что происходит, когда вы пишете:

Похоже, что сейчас мы замыкаем совпадение с шаблоном.

Теперь шаблоны просмотра следуют тому же принципу. Шаблон undefined -> x не будет оцениваться undefined на входных данных, так x как для достижения успеха не нужно знать результат undefined . Вместо undefined -> x:xs undefined -> [] этого, и undefined -> "yo" действительно нужно знать результат , следовательно, они будут оценивать его по мере необходимости.

О ваших примерах:

 f ((_:_) := (head -> y))
 

Здесь head -> y всегда все получается. Сам по себе он может привязываться y к нижнему значению, но этому препятствует крайний левый _:_ шаблон.

 f' ((head -> y) := (_:_))
 

Здесь head -> y всегда все получается. Сам по себе он будет привязан y к нижнему значению, и это действительно происходит, если ввод есть [] , но это не приведет к принудительному вводу, поэтому до сих пор не произошло сбоя. После этого мы пробуем самый левый _:_ шаблон, который терпит неудачу. Результат: сбой, но без сбоя.

 f'' (head -> y) = [ y ]
 

Опять же, head -> y всегда выполняется успешно и привязывается y к нижней части (если входные данные есть [] ). Сопоставление шаблонов будет успешным, и результат f'' будет [ head [] ] таким . Мы можем взять, например, длину этого списка, но мы не можем распечатать его содержимое без сбоя.

 f ((undefined -> "yo") := (x:_)) = [x]
f [] = []
 

undefined -> "yo" вылетает, как объяснялось выше. x:_ Шаблон никогда не опробован.

 f ((x:_) := (undefined -> "yo")) = [x]
 

Здесь мы впервые встречаемся x:_ , и только когда это удается, мы пытаемся undefined -> "yo" . Поскольку мы вызываем f с [] , шаблон представления не опробован, поэтому он не аварийно завершается. Вызов f "a" вместо этого будет совпадать x:_ , попробуйте шаблон представления и произойдет сбой.

Комментарии:

1. Пример немного странный, потому что в реальном случае undefined это функция, а не f .

2. @WheatWizard Я согласен. В некоторых случаях ваши собственные примеры используются undefined ->... в качестве шаблона представления, но в некоторых других случаях мне нужно объяснить, что происходит, когда вы передаете (частично) неопределенное значение функции, которая сопоставляет его с шаблоном.