Почему `forall (a::j) (b::k)` работает иначе, чем `forall (p::(j,k))`?

Я пытаюсь понять разницу между использованием forall для количественного определения двух переменных типа и использованием forall для количественного определения переменной одного типа типа кортежа.

Например, для следующих семейств типов:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}

type family Fst (p :: (a,b)) :: a where
  Fst '(a,_) = a
type family Snd (p :: (a,b)) :: b where
  Snd '(_,b) = b
type family Pair (p :: (Type,Type)) :: Type where
  Pair '(a,b) = (a,b)

Я могу определить идентификатор для пар, используя две переменные типа, и заставить его скомпилироваться на GHC 8.0.1:

ex0 :: forall (a :: Type) (b :: Type). Pair '(a,b) -> (Fst '(a,b), Snd '(a,b))
ex0 = id

Однако одно и то же определение не компилируется, если я использую переменную одного типа типа кортежа:

ex1 :: forall (p :: (Type,Type)). Pair p -> (Fst p, Snd p)
ex1 = id
-- Ex.hs:20:7: error:
--     • Couldn't match type ‘Pair p’ with ‘(Fst p, Snd p)’
--       Expected type: Pair p -> (Fst p, Snd p)
--         Actual type: (Fst p, Snd p) -> (Fst p, Snd p)
--     • In the expression: id
--       In an equation for ‘ex1’: ex1 = id
--     • Relevant bindings include
--         ex1 :: Pair p -> (Fst p, Snd p) (bound at Ex.hs:20:1)

Проблема в том, что p может быть ⊥?


haskell type-families forall
person rampion    schedule 14.12.2018    source источник

Ответы (2)


arrow_upward
3
arrow_downward

Причина просто в том, что на уровне типов нет проверки эта-преобразования. Начнем с того, что не существует механизма, позволяющего отличить data определения от записей/продуктов с одним конструктором, которые, возможно, имеют эта-законы. Я не думаю, что p, возможно, является ⊥ веской причиной для этого. Даже в частично ленивых языках сохраняется эта-равенство для пар (относительно наблюдательной эквивалентности).

person András Kovács    schedule 14.12.2018

arrow_upward
3
arrow_downward

Проблема в том, что p может быть ⊥?

Более менее. К сожалению, все виды обитают в семействе пустых типов.

type family Any :: k

Что расстраивает любую теорию, которая позволила бы сделать то, что вы пытаетесь сделать. Я думаю, что это действительно нужно исправить; Однако я не уверен, есть ли какие-либо планы сделать это.

person luqui    schedule 14.12.2018
comment
Any не должно быть проблемой. Если бы GHC преобразовал сопоставление записей уровня типов в примитивные проекции, как в Agda/Coq, то Any было бы неотличимо от (Fst Any, Snd Any), подтверждая правило эта. - person András Kovács; 14.12.2018
comment
@ AndrásKovács, ах, я понимаю, что ты имеешь в виду. Я думаю, что Any по-прежнему актуален, поскольку создает проблему для сопутствующих продуктов — или, например. если бы (,) были определены как тип data в Agda вместо record. - person luqui; 14.12.2018
comment
да, я имел в виду, что в данном случае это не проблема, но я думаю, что это также не является проблемой для сопутствующих продуктов, потому что, хотя Any делает недействительным эту побочного продукта, средства проверки типов в любом случае практически никогда не проверяют эту побочного продукта. (Но я также думаю, что было бы неплохо избавиться от Any). - person András Kovács; 14.12.2018
comment
@ AndrásKovács AndrásKovács, да, но в Agda, без нижних уровней типов (или каких-либо нижних), по крайней мере, есть возможность сопоставления с образцом, чтобы вы могли убедить свое определение пройти. Не так в Хаскеле. Но чем больше мы говорим, тем менее уместным для этого конкретного вопроса кажется мой комментарий, и это всего лишь моя общая обида. :-п - person luqui; 14.12.2018