Rodzaje zamkniętych rodzin i dziwne typy funkcji

Question

Niestety, nie mogłem sobie wyobrazić lepszego tytułu do tego pytania, więc proszę czytać dalej. Wyobraźmy sobie, że mamy zamkniętą rodzinę typ, który mapuje każdy rodzaj nim koresponduje Maybe wyjątkiem maybes się:

type family Family x where 
    Family (Maybe x) = Maybe x 
    Family x = Maybe x 

Możemy nawet zadeklarować funkcji przy użyciu tego typu family:

doMagic :: a -> Family a 
doMagic = undefined 

exampleA = doMagic $ Just() 
exampleB = doMagic $() 

grać z nim w GHCi pokazuje, że można ocenić rodzaj tej funkcji:

*Strange> :t exampleA  
exampleA :: Maybe()  
*Strange> :t exampleB  
exampleB :: Maybe()  

Pytanie brzmi, czy możliwe jest dostarczenie jakichkolwiek implementati funkcji doMagic z wyjątkiem undefined? Powiedzmy na przykład, że chciałbym zawrzeć każdą wartość w konstruktorze Just, oprócz Maybesa, który powinien pozostać nienaruszony, jak mógłbym to zrobić? Próbowałem używać typeclasses, ale nie udało mi się napisać kompilowanego podpisu dla funkcji doMagic, jeśli nie korzystałem z rodzin o zamkniętym typie, czy ktoś mógłby mi pomóc?

Answer 1

Można użyć innej rodziny zamkniętych typów, aby odróżnić Maybe x od x, a następnie można użyć innej typografii, aby zapewnić oddzielne implementacje doMagic dla tych dwóch przypadków.Szybka i brudna wersja:

{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, 
    FlexibleInstances, UndecidableInstances, ScopedTypeVariables #-} 

type family Family x where 
    Family (Maybe x) = Maybe x 
    Family x = Maybe x 

data True 
data False 

type family IsMaybe x where 
    IsMaybe (Maybe x) = True 
    IsMaybe x = False 


class DoMagic a where 
    doMagic :: a -> Family a 

instance (DoMagic' (IsMaybe a) a (Family a)) => DoMagic a where 
    doMagic = doMagic' (undefined :: IsMaybe a) 


class DoMagic' i a r where 
    doMagic' :: i -> a -> r 

instance DoMagic' True (Maybe a) (Maybe a) where 
    doMagic' _ = id 

instance DoMagic' False a (Maybe a) where 
    doMagic' _ = Just 


exampleA = doMagic $ Just() 
exampleB = doMagic $() 

Answer 2

Możesz wykonać funkcję doMagic, która kręci się wzdłuż. Niestety zamknięcie rodziny typów nie bardzo ci pomaga. Oto jak może wyglądać początek

{-# LANGUAGE TypeFamilies #-} 

type family Family x where 
    Family (Maybe x) = Maybe x 
    Family x = Maybe x 

class Magical a where doMagic :: a -> Family a 
instance Magical (Maybe a) where doMagic = id 
instance Magical() where doMagic = Just 

Można go zobaczyć w ghci pracuje tak jak prosiłeś:

*Main> doMagic $ Just() 
Just() 
*Main> doMagic $() 
Just() 

Więc dlaczego mówię to kuśtykając wzdłuż? Cóż, można zauważyć, że dwa przewidziane przypadki nie wyczerpują bardzo ekosystemu Haskell typów:

*Main> doMagic $ True 
<interactive>:3:1: 
    No instance for (Magical Bool) arising from a use of ‘doMagic’ 
    In the expression: doMagic 
    In the expression: doMagic $ True 
    In an equation for ‘it’: it = doMagic $ True 

Więc trzeba by zapewnić instancje dla każdego typu (konstruktora) interesów. Rzeczywiście, nie ma tu nawet niespójnych instancji - klubu, w którym można pokonać wiele takich problemów - pomaga tutaj; jeśli ktoś próbuje pisać

instance Magical (Maybe a) where doMagic = id 
instance Magical a where doMagic = Just 

kompilator słusznie skarży się, że po tym wszystkim nie wiemy, że w pełni polimorficzny instancji faktycznie ma odpowiedniego typu. Rzeczą niespójnych instancji jest to, że kompilator nie mówi nam, że tylko dlatego, że to była wybrana instancja, to inne instancje nie mają zastosowania. Możliwe więc, że w pewnym momencie wybieramy w pełni polimorficzną instancję, ale później odkrywamy, że byliśmy naprawdę za kulisami, a potem po prostu owinęliśmy jeden za dużo warstw Maybe wokół rzeczy. Niefortunny.

W tej chwili nie można wiele zrobić. Rodzaje zamkniętych typów w tym momencie po prostu nie zapewniają całej wiedzy, którą można chcieć mieć. Być może któregoś dnia GHC zaoferuje mechanizm, który sprawi, że rodziny typu zamkniętego będą bardziej użyteczne w tym zakresie, takie jak ograniczenie nierówności typu, ale nie wstrzymałbym się: to problem badawczy, jak dostarczyć tej użytecznej informacji, a ja nie ". usłyszeliśmy plotki o tym, jak ludzie się z tym uporali.