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

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

0 голосов
/ 14 декабря 2018

Я пытаюсь понять разницу между использованием 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 может быть ⊥?

Ответы [ 2 ]

0 голосов
/ 14 декабря 2018

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

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

type family Any :: k

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

0 голосов
/ 14 декабря 2018

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

...