Jak wskazuje tytuł pytania, chcę wiedzieć, czym jest polimorfizm Lewity i jaka jest jego motywacja? Wiem, że ta strona zawiera pewne szczegóły, ale większość wyjaśnień przechodzi przez moją głowę. :)
Chociaż ta strona jest trochę bardziej przyjazna, nadal nie jestem w stanie zrozumieć, jaka jest za nią motywacja.
Odpowiedzi:
Uwaga: ta odpowiedź jest oparta na bardzo niedawnych obserwacjach z dyskusji o Levity. Wszystko, co dotyczy polimorfizmu Levity, jest obecnie zaimplementowane tylko w kandydatach do wydania GHC 8.0 i jako takie może ulec zmianie (patrz na przykład # 11471 ).
TL; DR : Jest to sposób na uczynienie funkcji polimorficznymi względem typów podniesionych i unlifted, co nie jest możliwe w przypadku zwykłych funkcji. Na przykład poniższy kod nie sprawdza typów za pomocą zwykłych polimorfizmów, ponieważ Int#ma rodzaj #, ale zmienne typu idmają rodzaj *:
{-# LANGUAGE MagicHash #-}
import GHC.Prim
example :: Int# -> Int#
example = id -- does not work, since id :: a -> a
Couldn't match kind ‘*’ with ‘#’
When matching types
a0 :: *
Int# :: #
Expected type: Int# -> Int#
Actual type: a0 -> a0
In the expression: id
Zauważ, że (->)nadal używa trochę magii.
Zanim zacznę odpowiadać na to pytanie, niech nam zrobić krok do tyłu i przejść do jednego z najczęściej używanych funkcji ($).
Jaki jest ($)typ? Cóż, według Hackage i raportu, tak jest
($) :: (a -> b) -> a -> b
Jednak nie jest to ukończone w 100%. To wygodne małe kłamstwo. Problem polega na tym, że typy polimorficzne (jak ai b) mają rodzaj *. Jednak programiści (bibliotek) chcieli używać ($)nie tylko typów z rodzajem *, ale także takich #, np
unwrapInt :: Int -> Int#
Chociaż Intma rodzaj *(może być na dole), Int#ma rodzaj #(i wcale nie może być na dole). Mimo to sprawdza się następujący typ kodu:
unwrapInt $ 42
To nie powinno działać. Pamiętasz typ zwrotu ($)? Był polimorficzny, a typy polimorficzne są dobre *, nie #! Więc dlaczego to zadziałało? Najpierw był to błąd , a potem włamanie (fragment listu od Ryana Scotta z listy mailingowej ghc-dev):
Więc dlaczego tak się dzieje?
Długa odpowiedź jest taka, że przed GHC 8.0, w podpisie typu
($) :: (a -> b) -> a -> b,bfaktycznie nie było w naturze*, ale raczejOpenKind.OpenKindto okropny hack, który pozwala na zamieszkiwanie w nim zarówno podniesionym (uprzejmym*), jak i unlifted (kind#) typom, dlatego właśnie(unwrapInt $ 42)sprawdza się typy.
Więc jaki jest ($)nowy typ w GHC 8.0? Jego
($) :: forall (w :: Levity) a (b :: TYPE w). (a -> b) -> a -> b
-- will likely change according to Richard E.
Aby to zrozumieć, musimy spojrzeć na Levity:
data Levity = Lifted | Unlifted
Teraz możemy myśleć ($)o jednym z następujących typów, ponieważ są tylko dwie możliwości w:
-- pseudo types
($) :: forall a (b :: TYPE Lifted). (a -> b) -> a -> b
($) :: forall a (b :: TYPE Unlifted). (a -> b) -> a -> b
TYPEjest magiczną stałą, która na nowo definiuje rodzaje *i #jako
type * = TYPE Lifted
type # = TYPE Unlifted
Kwantyfikacja rodzajów jest również całkiem nowa i stanowi część integracji typów zależnych w Haskellu .
Nazwa polimorfizm Levity pochodzi z faktu, że teraz możesz pisać funkcje polimorficzne zarówno na typach podniesionych, jak i unlifted, co nie było dozwolone / możliwe przy poprzednich ograniczeniach dotyczących polimorfizmu. Jednocześnie pozbywa się OpenKindhacka. To naprawdę „tylko”, zajmując się obydwoma rodzajami.
Nawiasem mówiąc, nie jesteś sam ze swoim pytaniem. Nawet Simon Peyton Jones powiedział, że potrzebna jest strona wiki Levity , a Richard E. (obecny wykonawca tego) stwierdził, że strona wiki wymaga aktualizacji bieżącego procesu.
GHC.Types, część ghc-primbiblioteki dostarczanej z GHC.($) :: forall (w1 w2 :: Levity) (a :: TYPE w1) (b :: TYPE w2). (a -> b) -> a -> b, tj. Dlaczego ($)nie ma nadawać się do użytku z funkcjami z niezniesionymi argumentami?