Konieczność wrapperów typu egzystencjalnego

Question

Okazuje się, że zaskakująco trudno poprawnie używać typów egzystencjalnych/rang-n, pomimo bardzo prostego pomysłu.

Dlaczego owijanie typów egzystencjalnych w typy data jest konieczne?

mam następujący prosty przykład:

{-# LANGUAGE RankNTypes, ImpredicativeTypes, ExistentialQuantification #-} 
module Main where 

c :: Double 
c = 3 

-- Moving `forall` clause from here to the front of the type tuple does not help, 
-- error is the same 
lists :: [(Int, forall a. Show a => Int -> a)] 
lists = [ (1, \x -> x) 
     , (2, \x -> show x) 
     , (3, \x -> c^x) 
     ] 

data HRF = forall a. Show a => HRF (Int -> a) 

lists' :: [(Int, HRF)] 
lists' = [ (1, HRF $ \x -> x) 
     , (2, HRF $ \x -> show x) 
     , (3, HRF $ \x -> c^x) 
     ] 

Gdybym wykomentuj definicję lists, kod kompiluje pomyślnie. Jeśli go nie skomentuję, otrzymuję następujące błędy:

test.hs:8:21: 
    Could not deduce (a ~ Int) 
    from the context (Show a) 
     bound by a type expected by the context: Show a => Int -> a 
     at test.hs:8:11-22 
     `a' is a rigid type variable bound by 
      a type expected by the context: Show a => Int -> a at test.hs:8:11 
    In the expression: x 
    In the expression: \ x -> x 
    In the expression: (1, \ x -> x) 

test.hs:9:21: 
    Could not deduce (a ~ [Char]) 
    from the context (Show a) 
     bound by a type expected by the context: Show a => Int -> a 
     at test.hs:9:11-27 
     `a' is a rigid type variable bound by 
      a type expected by the context: Show a => Int -> a at test.hs:9:11 
    In the return type of a call of `show' 
    In the expression: show x 
    In the expression: \ x -> show x 

test.hs:10:21: 
    Could not deduce (a ~ Double) 
    from the context (Show a) 
     bound by a type expected by the context: Show a => Int -> a 
     at test.hs:10:11-24 
     `a' is a rigid type variable bound by 
      a type expected by the context: Show a => Int -> a at test.hs:10:11 
    In the first argument of `(^)', namely `c' 
    In the expression: c^x 
    In the expression: \ x -> c^x 
Failed, modules loaded: none. 

Dlaczego tak się dzieje? Czy drugi przykład nie powinien być równoważny pierwszemu? Jaka jest różnica między tymi zastosowaniami typów n-rangowych? Czy można w ogóle pominąć dodatkową definicję ADT i używać tylko prostych typów, gdy chcę tego rodzaju polimorfizm?

Answer 1

Istnieją dwie kwestie trzeba rozważyć należy obchodzić się z rodzajami egzystencjalnych:

• Jeśli przechowywać „wszystko, co może być show n”, masz do przechowywania rzeczy, które mogą być pokazany wraz z jak to pokazać.
• Zmienna rzeczywista może mieć tylko jeden typ.

Pierwszym punktem jest to, dlaczego trzeba mieć egzystencjalne owijarki typu, ponieważ kiedy piszesz tak:

data Showable = Show a => Showable a 

Co właściwie się dzieje, że coś takiego zostanie ogłoszony:

data Showable a = Showable (instance of Show a) a 

To znaczy odniesienie do instancji klasy Show a jest przechowywane wraz z wartością a. Bez tego nie można mieć funkcji, która rozpakowuje Showable, ponieważ ta funkcja nie wie, jak wyświetlić a.

Po drugie, czasami pojawia się pewne dziwactwo typu i dlaczego nie można na przykład powiązać typów egzystencji w wiązaniach let.

---

Masz również problem z rozumowaniem w swoim kodzie. Jeśli masz funkcję jak forall a . Show a => (Int -> a) masz funkcję, która, biorąc pod uwagę dowolną liczbą całkowitą, będzie w stanie wyprodukować każdy rodzaj wartości showable że dzwoniący wybierze. Prawdopodobnie masz na myśli exists a . Show a => (Int -> a), co oznacza, że ​​jeśli funkcja otrzyma liczbę całkowitą, zwróci ona pewien typ, dla którego istnieje instancja Show.

Answer 2

Przykłady nie są równoważne. Pierwszy

lists :: [(Int, forall a. Show a => Int -> a)] 

mówi, że każda druga część może wytwarzać dowolnego rodzaju, pod warunkiem, że jest to przykład Show z Int.

Drugim przykładem jest modulo odpowiednik typu wrapper do

lists :: [(Int, exists a. Show a => Int -> a)] 

czyli każdy drugi składnik może produkować trochę typ należącej do Show z Int, ale nie masz pojęcia który typ tej funkcji zwraca.

Dalsze funkcje można umieścić w krotek nie spełniają pierwszy kontrakt:

lists = [ (1, \x -> x) 
     , (2, \x -> show x) 
     , (3, \x -> c^x) 
     ] 

\x -> x produkuje ten sam typ co powoduje, że jest on podany jako dane wejściowe, więc tutaj, to Int. show zawsze produkuje String, więc jest to jeden stały typ. wreszcie, \x -> c^x wytwarza ten sam typ co c, a mianowicie Double.

Answer 3

Twoja pierwsza próba jest nie użyciu typów egzystencjalne. Raczej twoi

lists :: [(Int, forall a. Show a => Int -> a)] 

żądania że drugi składnik mogą zapewnić elementem żadnego showable typ, który wybiorę, nie tylko niektóre showable typu, który wybierzesz. Szukamy

ale to nie jest to, co powiedziałeś. Metoda pakowania typów danych pozwala odzyskać exists z forall przez curry. Trzeba

HRF :: forall a. Show a => (Int -> a) -> HRF 

co oznacza, że ​​aby budować wartość HRF, trzeba dostarczać potrójną zawierającą typ a, słownik Show dla a i funkcję w Int -> a. Oznacza to wpisz HRF konstruktora skutecznie curry Ten przeznaczony dla typu

HRF :: (exists a. Show a * (Int -> a)) -> HRF -- not real Haskell 

może być w stanie uniknąć metody typu danych przy użyciu typów ranga-N Church zakodować egzystencjalny

type HRF = forall x. (forall a. Show a => (Int -> a) -> x) -> x 

ale to prawdopodobnie przesada.