Dlaczego Djinn nie realizuje typowych funkcji monadycznych?

Question

Niedawno natknąłem się na Djinn i krótko się z nim bawiłem, aby sprawdzić, czy będzie to przydatne w moim codziennym obiegu kodowania. Byłem podekscytowany widząc, że Djinn miał monady i próbował sprawdzić, czy może znaleźć jakieś fajne funkcje.

Dżin zrobił naprawdę cuda. Sygnatura typu początkowo (przynajmniej dla mnie) nieintuicyjna funkcja jest >>= (>>=). Djinn był w stanie natychmiast demystify to stwierdzając

Djinn> f ? Monad m => ((a -> m b) -> m a) -> (a -> m b) -> m b 
f :: (Monad m) => ((a -> m b) -> m a) -> (a -> m b) -> m b 
f a b = a b >>= b 

Niestety, dżin nie może wydawać się znaleźć inne standardowe funkcje na monad, mimo wiedząc o typeclass Monad.

• join (który powinien być join = (>>= id) lub Bardziej szczegółowa składni dżin w join a = a >>= (\x -> x))

  Djinn> join ? Monad m => m (m a) -> m a 
  -- join cannot be realized. 
  

• liftM (który powinien być liftM f = (>>= (return . f)) lub składni Bardziej szczegółowa dżin w liftM a b = b >>= (\x -> return (a x)))

  Djinn> liftM ? Monad m => (a -> b) -> m a -> m b 
  -- liftM cannot be realized. 
  

• Nawet podstawowy return :: Monad m => m a -> m (m a) nie może znaleźć Djinn lub return :: Monad m => (a, b) -> m (a, b).

  Djinn> f ? Monad m => (a, b) -> m (a, b) 
  -- f cannot be realized. 
  

Djinn umie wykorzystać \ skonstruować funkcje anonimowe, więc dlaczego tak się dzieje?

Mój szorstki podejrzenie, że być może Djinn ma uproszczone pojęcie typeclass i jakoś traktuje m a jako „stałe” tak, że m (a, b) nie jest postrzegane jako przypadek m a, ale nie mam pojęcia jak zrobić, że każdy bardziej konkretne niż jego aktualna, ręcznie falista forma, czy ta intuicja jest poprawna.

Answer 1

Wspieranie klas typów właściwie wygląda bardzo podobnie do wspierania typów rangi 2; porównaj:

join :: Monad m 
    => m (m a) -> m a 

vs:

join :: (forall a. a -> m a) 
    -> (forall a b. m a -> (a -> m b) -> m b) 
    -> m (m a) -> m a 

Niestety, techniki Djinn używa nie obsługiwać szeregowych 2 typy w ogóle. Jeśli float foralls tak że Djinn może go przetworzyć, nagle to, co otrzymujemy w zamian są betonowe wybory:

join :: (b -> m b) 
    -> (m c -> (c -> m d) -> m d) 
    -> m (m a) -> m a 

który wygląda dużo mniej jak można go wdrożyć! Jeśli powiesz Djinnowi, z których wystąpień korzystać, to oczywiście działa znacznie lepiej.

join :: (b -> m b) 
    -> (m (m a) -> (m a -> m a) -> m a) 
    -> m (m a) -> m a 

W tym przypadku Djinn dokona właściwego wdrożenia. ... ale to jest oszustwo.