Zrozumienie Operatora obsady Haskella

Question

Załóżmy, że zaimportowaliśmy Data.Typeable, który zawiera cast :: (Typeable a, Typeable b) -> a -> Maybe b.

Uważają, że

> cast 'n' :: Maybe Char 
Just 'n' 

jeszcze

> cast 7 :: Maybe Char 
Nothing 

Rozumiem wyżej, ale wydaje się być banalnym przykładem. Nie ujawnia, dlaczego ktoś musiałby użyć operatora cast (o ile widzę).

Pytanie: Czy jest przykładem wykorzystania cast które faktycznie „zmiany” typ wartości z jednego typu na inny? Najbliższy przykład mogę myśleć (co w rzeczywistości nie działa w GHCi) byłaby zmiana typu 7 z Integer do Double:

> cast 7 :: Maybe Double 
Just '7' -- this doesn't work, as 7 is typed as a Integer above; instead GHCi returns Nothing 

Answer 1

Czy jest przykładem wykorzystania obsady, która autentycznie " zmienia "typ wartości z jednego typu na inny?

Prosta odpowiedź brzmi: nie. Ale może istnieć sytuacja, w której nie znasz swojego typu, ponieważ jest on "ukryty" przez kwantyfikator "istnieje". Oto przykład:

{-# LANGUAGE ExistentialQuantification #-} 

import Data.Typeable 
import Data.Maybe 

data Foo = forall a . Typeable a => Foo a 

main = print . catMaybes . map (\(Foo x) -> cast x :: Maybe Bool) $ xs 
    where 
    xs = [Foo True, Foo 'a', Foo "str", Foo False] 

wyjście będzie:

[True,False] 

Answer 2

Celem klasy Typeable jest pozwalają na pracę z danymi, jeśli nie znamy jej dokładnej typu. Zadaniem operatora cast jest sprawdzenie, czy niektóre dane mają określony typ, a jeśli tak, pozwól na pracę z tym typem. Wszystko zależy od robienia rzeczy pod typu podpisu z twoich danych. Rzeczywista wartość nie zmienia się wcale.

Jeśli chcesz zmienić wartość niektórych danych, że nie jest to odlew, to jest konwersja. Wszelkiego rodzaju funkcje, które mogą to robić. Np., fromIntegral przekształca coś, co jest instancją Integral w coś innego. (Np., Int do Double.) To nie jest to, co oznacza odlewanie.

Answer 3

Załóżmy, że chcesz zaimplementować funkcję, która działa jako funkcja tożsamości dla wszystkich wartości, z wyjątkiem liczb całkowitych, w których powinna pełnić funkcję następczą.

W pozbawionym typu języka jak Python, jest prosta:

>>> def f(x): 
... if type(x) == int: 
...  return x+1 
... else: 
...  return x 
... 
>>> f(42) 
43 
>>> f("qwerty") 
'qwerty' 

Nawet w Javie, jest to wykonalne, nawet jeśli wymaga to trochę rzucania:

static <A> A f(A a) { 
    if (a instanceof Integer) 
     return (A) (Integer) ((Integer) a + 1); 
    else 
     return a; 
} 

public static void main (String[] args) throws java.lang.Exception 
{ 
    System.out.println(">> " + f(42)); 
    System.out.println(">> " + f("qwerty")); 
} 

/* Output: 
>> 43 
>> qwerty 
*/ 

Co o Haskell?

W programie Haskell nie można tego zrobić.Dowolna funkcja typu forall a. a -> a musi albo przestać się kończyć, albo zachowywać się jak tożsamość. Jest to bezpośrednia konsekwencja skojarzenia tego typu z free theorem.

Jednakże, jeśli możemy dodać Typeable ograniczenie typu a, wówczas staje się możliwe:

f :: forall a. Typeable a => a -> a 
f x = case cast x :: Maybe Int of 
    Nothing -> x 
    Just n -> case cast (n+1) :: Maybe a of 
     Nothing -> x 
     Just y -> y 

Pierwszy cast konwertuje a do Int, drugi cast konwertuje a powrotem do Int.

Powyższy kod jest dość brzydki, ponieważ wiemy, że druga obsada nie może zawieść, więc nie ma żadnej potrzeby na drugą obsadę. Możemy poprawić powyższy kod z eqT i GADT typu równości:

f :: forall a. Typeable a => a -> a 
f x = case eqT :: Maybe (a :~: Int) of 
    Nothing -> x 
    Just Refl -> x+1 

Zasadniczo eqT mówi nam, czy dwa typy (Typeable) są równe. Nawet lepiej, po dopasowaniu z Just Refl, kompilator wie również, że są one równe i pozwala nam używać wartości Int zamiast wartości a, zamiennie i bez rzutowania.

Rzeczywiście, dzięki GADTs, :~: i eqT, teraz większość zastosowań cast są teraz nieaktualne. cast samo można trywialnie realizowane z eqT:

cast :: forall a. (Typeable a, Typeable b) => a -> Maybe b 
cast x = case eqT :: Maybe (a :~: b) of 
    Nothing -> Nothing 
    Just Refl -> Just x 

Wniosek: w Haskell, mamy najlepsze z obu świata. Posiadamy gwarancje parametryczności (twierdzenia wolne) dla typów polimorficznych. Możemy także złamać te gwarancje parametryczności i zastosować polimorfizm "ad hoc", za cenę dodatkowego ograniczenia Typeable.