Czy mogę wydrukować w Haskell taki typ funkcji polimorficznej, jaką stałoby się, gdybym przekazał do niej jednostkę konkretnego typu?

Dec 12 2020

Oto funkcja polimorficzna w 3 typach:

:t (.)
(.) :: (b -> c) -> (a -> b) -> a -> c

a tutaj funkcja niepolimorficzna:

:t Data.Char.digitToInt
Data.Char.digitToInt :: Char -> Int

Jeśli zastosujemy to pierwsze do drugiego, otrzymamy funkcję polimorficzną w 1 typie:

:t (.) Data.Char.digitToInt
(.) Data.Char.digitToInt :: (a -> Char) -> a -> Int

co oznacza, że (.)został „utworzony” (nie jestem pewien, czy to jest poprawny termin; jako programista C ++ tak to nazwałbym) z b === Chari c === Int, więc podpis tego, do (.)którego zostanie zastosowany, digitToIntjest następujący

(Char -> Int) -> (a -> Char) -> a -> Int

Moje pytanie brzmi: czy jest jakiś sposób, aby ten podpis drukowany na ekranie, biorąc pod uwagę (.), digitToInta „informacje”, że chcę zastosować były do tej ostatniej?

Dla zainteresowanych to pytanie zostało wcześniej zamknięte jako duplikat tego .

Odpowiedzi

7 MikeSpivey Dec 13 2020 at 06:32

Inne odpowiedzi wymagają pomocy funkcji, które zostały zdefiniowane za pomocą sztucznie ograniczonych typów, takich jak asTypeOffunkcja w odpowiedzi z HTNW. Nie jest to konieczne, jak pokazuje następująca interakcja:

Prelude> let asAppliedTo f x = const f (f x)

Prelude> :t head `asAppliedTo` "x"
head `asAppliedTo` "x" :: [Char] -> Char

Prelude> :t (.) `asAppliedTo` Data.Char.digitToInt
(.) `asAppliedTo` Data.Char.digitToInt
  :: (Char -> Int) -> (a -> Char) -> a -> Int

Wykorzystuje to brak polimorfizmu w wiązaniu lambda, który jest domniemany w definicji asAppliedTo. Oba wystąpienia fw jego ciele muszą mieć ten sam typ i taki jest typ wyniku. Zastosowana consttutaj funkcja również ma swój naturalny typ a -> b -> a:

const x y = x
12 HTNW Dec 12 2020 at 09:09

Jest taka zgrabna mała funkcja ukryta w rogu Prelude:

Prelude.asTypeOf :: a -> a -> a
asTypeOf x _ = x

Jest to udokumentowane jako „wymuszanie tego samego typu pierwszego argumentu, co drugi”. Możemy użyć tego do wymuszenia typu (.)pierwszego argumentu:

-- (.) = \x -> (.) x = \x -> (.) $ x `asTypeOf` Data.Char.digitToInt -- eta expansion followed by definition of asTypeOf -- the RHS is just (.), but restricted to arguments with the same type as digitToInt -- "what is the type of (.) when the first argument is (of the same type as) digitToInt?" ghci> :t \x -> (.) $ x `asTypeOf` Data.Char.digitToInt
\x -> (.) $ x `asTypeOf` Data.Char.digitToInt
  :: (Char -> Int) -> (a -> Char) -> a -> Int

Oczywiście działa to w przypadku tylu argumentów, ile potrzebujesz.

ghci> :t \x y -> (x `asTypeOf` Data.Char.digitToInt) . (y `asTypeOf` head)
\x y -> (x `asTypeOf` Data.Char.digitToInt) . (y `asTypeOf` head)
  :: (Char -> Int) -> ([Char] -> Char) -> [Char] -> Int

Możesz uznać to za odmianę pomysłu @ KABuhr w komentarzach - używając funkcji z podpisem bardziej restrykcyjnym niż jej implementacja, aby kierować wnioskami o typie - z wyjątkiem tego, że nie musimy niczego definiować sami, kosztem niemożności po prostu skopiuj dane wyrażenie pod lambdą.

8 K.A.Buhr Dec 12 2020 at 09:57

Myślę, że odpowiedź @ HTNW prawdopodobnie to obejmuje, ale dla kompletności, oto jak inContextszczegółowo działa to rozwiązanie.

Podpis typu funkcji:

inContext :: a -> (a -> b) -> a

oznacza, że ​​jeśli masz coś, co chcesz wpisać, i „kontekst”, w którym jest używany (wyrażany jako lambda przyjmująca ją jako argument), powiedz z typami:

thing :: a1
context :: a2 -> b

Możesz wymusić ujednolicenie a1(ogólnego typu thing) z a2(ograniczeniami kontekstu), po prostu konstruując wyrażenie:

thing `inContext` context

Zwykle ujednolicony typ thing :: azostałby utracony, ale sygnatura typu inContextoznacza, że ​​typ całego tego wyrażenia wynikowego będzie również ujednolicony z żądanym typem a, a GHCi z radością poinformuje Cię o typie tego wyrażenia.

A więc wyrażenie:

(.) `inContext` \hole -> hole digitToInt

kończy się przypisaniem typu, który (.)miałby w określonym kontekście. Możesz to napisać nieco myląco, jako:

(.) `inContext` \(.) -> (.) digitToInt

ponieważ (.)jest równie dobrą nazwą argumentu dla anonimowej lambdy, jak holejest. Jest to potencjalnie mylące, ponieważ tworzymy lokalne powiązanie, które przesłania definicję najwyższego poziomu (.), ale nadal nazywa to samo (z wyrafinowanym typem), a to nadużycie lambd pozwoliło nam napisać oryginalne wyrażenie (.) digitToIntdosłownie, z odpowiednim wzorcem.

Właściwie nie ma znaczenia, w jaki sposób inContextjest zdefiniowany, jeśli pytasz tylko GHCi o jego typ, więc inContext = undefinedzadziałałoby. Ale patrząc na podpis typu, łatwo jest podać inContextroboczą definicję:

inContext :: a -> (a -> b) -> a
inContext a _ = a

Okazuje się, że to tylko definicja const, więc też inContext = constdziała.

Możesz użyć inContextdo wpisania wielu rzeczy naraz i mogą to być wyrażenia zamiast nazw. Aby dostosować się do tego pierwszego, możesz użyć krotek; aby ta ostatnia działała, musisz użyć bardziej rozsądnych nazw argumentów w swoich lambdach.

Na przykład:

λ> :t (fromJust, fmap length) `inContext` \(a,b) -> a . b
(fromJust, fmap length) `inContext` \(a,b) -> a . b
  :: Foldable t => (Maybe Int -> Int, Maybe (t a) -> Maybe Int)

informuje, że w wyrażeniu fromJust . fmap lengthtypy zostały wyspecjalizowane do:

fromJust :: Maybe Int -> Int
fmap length :: Foldable t => Maybe (t a) -> Maybe Int
6 FyodorSoikin Dec 12 2020 at 03:35

Możesz to zrobić za pomocą TypeApplicationsrozszerzenia, które pozwala jawnie określić, których typów chcesz użyć do utworzenia wystąpienia parametrów typu:

λ :set -XTypeApplications                                 
λ :t (.) @Char @Int
(.) @Char @Int :: (Char -> Int) -> (a -> Char) -> a -> Int

Zwróć uwagę, że argumenty muszą mieć dokładną kolejność.

W przypadku funkcji, które mają podpis typu „zwykłego”, np foo :: a -> b. Kolejność jest definiowana przez kolejność, w jakiej parametry typu pojawiają się po raz pierwszy w podpisie.

W przypadku funkcji, które używają ExplicitForalllike foo :: forall b a. a -> b, kolejność jest definiowana przez to, w czym się znajduje forall.


Jeśli chcesz dowiedzieć się, jaki typ jest konkretnie w oparciu o zastosowanie (.)do digitToChar(w przeciwieństwie do zwykłej wiedzy, które typy wypełnić), jestem prawie pewien, że nie możesz tego zrobić w GHCi, ale mogę bardzo polecić obsługę Haskell IDE.

Na przykład, tak to wygląda dla mnie w VSCode (tutaj jest rozszerzenie ):

5 chi Dec 12 2020 at 16:39

Jest to niewielka odmiana odpowiedzi HTNW.

Załóżmy, że mamy dowolne, potencjalnie duże, wyrażenie zawierające identyfikator polimorficzny poly

 .... poly ....

i zastanawiamy się, jak w tym momencie utworzono wystąpienie typu polimorficznego.

Można to zrobić wykorzystując dwie cechy GHC: asTypeOf(o czym wspomina HTNW) i wpisane dziury w następujący sposób:

 .... (poly `asTypeOf` _) ....

Po odczytaniu _otworu GHC wygeneruje błąd informujący o rodzaju terminu, który należy wprowadzić w miejsce tego otworu. Ponieważ używaliśmy asTypeOf, musi to być to samo, co typ konkretnego wystąpienia, polyktórego potrzebujemy w tym kontekście.

Oto przykład w GHCi:

> ((.) `asTypeOf` _) Data.Char.digitToInt
<interactive>:11:17: error:
    * Found hole: _ :: (Char -> Int) -> (a -> Char) -> a -> Int