Rozważ tę reprezentację dla wyrażeń lambda sparametryzowanych przez ich wolne zmienne. (Patrz artykuły Bellegarde i Hook 1994, Bird i Paterson 1999, Altenkirch i Reus 1999.)
data Tm a = Var a
| Tm a :$ Tm a
| Lam (Tm (Maybe a))
Z pewnością możesz to uczynić Functor, przechwytując pojęcie zmiany nazwy i Monadprzechwytując pojęcie zastępowania.
instance Functor Tm where
fmap rho (Var a) = Var (rho a)
fmap rho (f :$ s) = fmap rho f :$ fmap rho s
fmap rho (Lam t) = Lam (fmap (fmap rho) t)
instance Monad Tm where
return = Var
Var a >>= sig = sig a
(f :$ s) >>= sig = (f >>= sig) :$ (s >>= sig)
Lam t >>= sig = Lam (t >>= maybe (Var Nothing) (fmap Just . sig))
Rozważmy teraz zamknięte warunki: to są mieszkańcy Tm Void. Powinieneś być w stanie osadzić zamknięte warunki w terminach z dowolnymi wolnymi zmiennymi. W jaki sposób?
fmap absurd :: Tm Void -> Tm a
Haczyk polega oczywiście na tym, że ta funkcja przejdzie przez termin dokładnie nic nie robiąc. Ale to odrobinę bardziej szczere niż unsafeCoerce. I dlatego vacuouszostał dodany do Data.Void...
Lub napisz ewaluatora. Oto wartości z wolnymi zmiennymi w b.
data Val b
= b :$$ [Val b] -- a stuck application
| forall a. LV (a -> Val b) (Tm (Maybe a)) -- we have an incomplete environment
Przedstawiłem właśnie lambdy jako zamknięcia. Ewaluator jest parametryzowany przez środowisko odwzorowujące wolne zmienne ana wartości powyżej b.
eval :: (a -> Val b) -> Tm a -> Val b
eval g (Var a) = g a
eval g (f :$ s) = eval g f $$ eval g s where
(b :$$ vs) $$ v = b :$$ (vs ++ [v]) -- stuck application gets longer
LV g t $$ v = eval (maybe v g) t -- an applied lambda gets unstuck
eval g (Lam t) = LV g t
Zgadłeś. Aby ocenić zamknięty termin w dowolnym celu
eval absurd :: Tm Void -> Val b
Mówiąc bardziej ogólnie, Voidjest rzadko używany samodzielnie, ale jest przydatny, gdy chcesz utworzyć wystąpienie parametru typu w sposób wskazujący na jakąś niemożliwość (np. Tutaj, używając wolnej zmiennej w zamkniętym terminie). Często te parametryzowane typy pochodzą z funkcji wyższego rzędu operacji podnoszenia od parametrów operacji na całym typu (na przykład tutaj fmap, >>=, eval). Więc przekazujesz absurdjako operację ogólnego przeznaczenia Void.
Na przykład, wyobraź sobie użycie Either e vdo przechwytywania obliczeń, które, miejmy nadzieję, dają ci, vale mogą wywołać wyjątek typu e. Możesz użyć tego podejścia do jednolitego dokumentowania ryzyka złego zachowania. Aby uzyskać doskonale wykonane obliczenia w tym ustawieniu, weź eje Void, a następnie użyj
either absurd id :: Either Void v -> v
bezpiecznie biegać lub
either absurd Right :: Either Void v -> Either e v
aby osadzić bezpieczne komponenty w niebezpiecznym świecie.
Aha, i ostatni hurra, radzenie sobie z „nie może się zdarzyć”. Pojawia się w ogólnej konstrukcji zamka błyskawicznego, wszędzie tam, gdzie nie może znajdować się kursor.
class Differentiable f where
type D f :: * -> * -- an f with a hole
plug :: (D f x, x) -> f x -- plugging a child in the hole
newtype K a x = K a -- no children, just a label
newtype I x = I x -- one child
data (f :+: g) x = L (f x) -- choice
| R (g x)
data (f :*: g) x = f x :&: g x -- pairing
instance Differentiable (K a) where
type D (K a) = K Void -- no children, so no way to make a hole
plug (K v, x) = absurd v -- can't reinvent the label, so deny the hole!
Postanowiłem nie usuwać reszty, mimo że nie jest to do końca istotne.
instance Differentiable I where
type D I = K ()
plug (K (), x) = I x
instance (Differentiable f, Differentiable g) => Differentiable (f :+: g) where
type D (f :+: g) = D f :+: D g
plug (L df, x) = L (plug (df, x))
plug (R dg, x) = R (plug (dg, x))
instance (Differentiable f, Differentiable g) => Differentiable (f :*: g) where
type D (f :*: g) = (D f :*: g) :+: (f :*: D g)
plug (L (df :&: g), x) = plug (df, x) :&: g
plug (R (f :&: dg), x) = f :&: plug (dg, x)
Właściwie może to ma znaczenie. Jeśli masz ochotę na przygodę, ten niedokończony artykuł pokazuje, jak Voidskompresować reprezentację terminów za pomocą wolnych zmiennych
data Term f x = Var x | Con (f (Term f x)) -- the Free monad, yet again
w dowolnej składni generowanej swobodnie z funktora Differentiablei . Używamy do reprezentowania regionów bez wolnych zmiennych i do przedstawiania tuneli rurowych przez regiony bez wolnych zmiennych albo do izolowanej zmiennej wolnej, albo do skrzyżowania ścieżek do dwóch lub więcej zmiennych wolnych. Muszę kiedyś skończyć ten artykuł.TraversablefTerm f Void[D f (Term f Void)]
Dla typu bez wartości (a przynajmniej takich, o których warto mówić w grzecznym towarzystwie), Voidjest niezwykle przydatne. I absurdjak tego używasz.
absurdfunkcja została użyta w tym artykule dotyczącymContmonady: haskellforall.com/2012/12/the-continuation-monad.html