Ответ 1
Изменить. Я вспомнил очень полезный факт о логарифмах и деривативах, которые я обнаружил, пока отвратительно висел на другом диване. К сожалению, этот друг (покойный великий Костас Турлас) уже не с нами, но я помню его, отвратительно вися на другом диване друга.
Позвольте напомнить себе о попытках. (Многие из моих товарищей работали над этими структурами в ранних новизнах: Ральф Хинзе, Торстен Альтенкирх и Питер Хэнкок spring сразу на ум в этом отношении.) Что действительно происходит, так это то, что мы вычисляем экспоненту типа t
, помня, что t -> x
является способом записи x
^ t
.
То есть мы ожидаем оснастить тип t
функтором Expo t
таким образом, чтобы Expo t x
представлял t -> x
. Мы должны ожидать, что Expo t
будет аппликативным (zippily). Изменить: Хэнкок называет такие функторы "Naperian", потому что они имеют логарифмы, и они применяются так же, как и функции, причем pure
является комбинатором K, а <*>
- S. что Expo t ()
должно быть изоморфным с ()
, причем const (pure ())
и const ()
выполняют (не много) работу.
class Applicative (Expo t) => EXPO t where
type Expo t :: * -> *
appl :: Expo t x -> (t -> x) -- trie lookup
abst :: (t -> x) -> Expo t x -- trie construction
Другой способ выразить это то, что t
является логарифмом Expo t
.
(Я почти забыл: поклонники исчисления должны проверить, что t
изоморфен ∂ (Expo t) ()
. Этот изоморфизм может быть весьма полезным. Изменить: он чрезвычайно полезен, и мы добавим его до EXPO
позже.)
Нам понадобится материал для набора компонентов. Функтор тождества является zippiy аппликативным...
data I :: (* -> *) where
I :: x -> I x
deriving (Show, Eq, Functor, Foldable, Traversable)
instance Applicative I where
pure x = I x
I f <*> I s = I (f s)
... и его логарифм является единичным типом
instance EXPO () where
type Expo () = I
appl (I x) () = x
abst f = I (f ())
Продукты zippy-аппликаций zippily applative...
data (:*:) :: (* -> *) -> (* -> *) -> (* -> *) where
(:*:) :: f x -> g x -> (f :*: g) x
deriving (Show, Eq, Functor, Foldable, Traversable)
instance (Applicative p, Applicative q) => Applicative (p :*: q) where
pure x = pure x :*: pure x
(pf :*: qf) <*> (ps :*: qs) = (pf <*> ps) :*: (qf <*> qs)
... и их логарифмы представляют собой суммы.
instance (EXPO s, EXPO t) => EXPO (Either s t) where
type Expo (Either s t) = Expo s :*: Expo t
appl (sf :*: tf) (Left s) = appl sf s
appl (sf :*: tf) (Right t) = appl tf t
abst f = abst (f . Left) :*: abst (f . Right)
Композиции zippy-аппликаций zippily аппликативные...
data (:<:) :: (* -> *) -> (* -> *) -> (* -> *) where
C :: f (g x) -> (f :<: g) x
deriving (Show, Eq, Functor, Foldable, Traversable)
instance (Applicative p, Applicative q) => Applicative (p :<: q) where
pure x = C (pure (pure x))
C pqf <*> C pqs = C (pure (<*>) <*> pqf <*> pqs)
и их логарифмы являются произведениями.
instance (EXPO s, EXPO t) => EXPO (s, t) where
type Expo (s, t) = Expo s :<: Expo t
appl (C stf) (s, t) = appl (appl stf s) t
abst f = C (abst $ \ s -> abst $ \ t -> f (s, t))
Если мы включим достаточно материала, мы можем теперь написать
newtype Tree = Tree (Either () (Tree, Tree))
deriving (Show, Eq)
pattern Leaf = Tree (Left ())
pattern Node l r = Tree (Right (l, r))
newtype ExpoTree x = ExpoTree (Expo (Either () (Tree, Tree)) x)
deriving (Show, Eq, Functor, Applicative)
instance EXPO Tree where
type Expo Tree = ExpoTree
appl (ExpoTree f) (Tree t) = appl f t
abst f = ExpoTree (abst (f . Tree))
Тип TreeMap a
в вопросе, будучи
data TreeMap a
= TreeMap {
tm_leaf :: Maybe a,
tm_node :: TreeMap (TreeMap a)
}
точно Expo Tree (Maybe a)
, причем lookupTreeMap
является flip appl
.
Теперь, учитывая, что Tree
и Tree -> x
- это совсем другие вещи, мне кажется странным, что код работает "на обоих". Тест равенства деревьев является особым случаем поиска только в том смысле, что тест равенства деревьев - это любая старая функция, действующая на дерево. Однако есть совпадение совпадений: чтобы проверить равенство, мы должны превратить каждое дерево в собственный самопознаватель. Изменить:, что именно то, что log-diff iso
делает.
Структура, которая дает тест равенства, - это некоторое понятие соответствия. Вот так:
class Matching a b where
type Matched a b :: *
matched :: Matched a b -> (a, b)
match :: a -> b -> Maybe (Matched a b)
То есть мы ожидаем, что Matched a b
будет представлять собой как-то пару из a
и a b
, которые совпадают. Мы должны иметь возможность извлечь пару (забыв, что они совпадают), и мы должны иметь возможность брать любую пару и пытаться их сопоставить.
Неудивительно, что мы можем сделать это для типа единицы, довольно успешно.
instance Matching () () where
type Matched () () = ()
matched () = ((), ())
match () () = Just ()
Для продуктов мы работаем покомпонентно, поскольку единственная опасность представляет собой несоответствие компонентов.
instance (Matching s s', Matching t t') => Matching (s, t) (s', t') where
type Matched (s, t) (s', t') = (Matched s s', Matched t t')
matched (ss', tt') = ((s, t), (s', t')) where
(s, s') = matched ss'
(t, t') = matched tt'
match (s, t) (s', t') = (,) <$> match s s' <*> match t t'
Суммы предлагают некоторую вероятность несоответствия.
instance (Matching s s', Matching t t') =>
Matching (Either s t) (Either s' t') where
type Matched (Either s t) (Either s' t')
= Either (Matched s s') (Matched t t')
matched (Left ss') = (Left s, Left s') where (s, s') = matched ss'
matched (Right tt') = (Right t, Right t') where (t, t') = matched tt'
match (Left s) (Left s') = Left <$> match s s'
match (Right t) (Right t') = Right <$> match t t'
match _ _ = Nothing
Интересно, что теперь мы можем получить тест равенства для деревьев так же легко, как
instance Matching Tree Tree where
type Matched Tree Tree = Tree
matched t = (t, t)
match (Tree t1) (Tree t2) = Tree <$> match t1 t2
(Кстати, подкласс Functor
, который фиксирует понятие соответствия, будучи
class HalfZippable f where -- "half zip" comes from Roland Backhouse
halfZip :: (f a, f b) -> Maybe (f (a, b))
к сожалению, пренебрегают. Морально, для каждого такого f
мы должны иметь
Matched (f a) (f b) = f (Matched a b)
Веселое упражнение - показать, что если (Traversable f, HalfZippable f)
, то свободная монада на f
имеет алгоритм унификации первого порядка.)
Я предполагаю, что мы можем построить "списки ассоциаций одиночной сети" следующим образом:
mapOne :: forall a. (Tree, a) -> Expo Tree (Maybe a)
mapOne (t, a) = abst f where
f :: Tree -> Maybe a
f u = pure a <* match t u
И мы могли бы попытаться объединить их с этим гаджетом, используя zippiness всех Expo t
s...
instance Monoid x => Monoid (ExpoTree x) where
mempty = pure mempty
mappend t u = mappend <$> t <*> u
... но, опять же, полная глупость экземпляра Monoid
для Maybe x
продолжает расстраивать чистый дизайн.
Мы можем по крайней мере управлять
instance Alternative m => Alternative (ExpoTree :<: m) where
empty = C (pure empty)
C f <|> C g = C ((<|>) <$> f <*> g)
Забавное упражнение состоит в том, чтобы слить abst
с match
, и, возможно, это то, на что действительно стоит вопрос. Пусть рефакторинг Matching
.
class EXPO b => Matching a b where
type Matched a b :: *
matched :: Matched a b -> (a, b)
match' :: a -> Proxy b -> Expo b (Maybe (Matched a b))
data Proxy x = Poxy -- I'm not on GHC 8 yet, and Simon needs a hand here
Для ()
, что нового является
instance Matching () () where
-- skip old stuff
match' () (Poxy :: Proxy ()) = I (Just ())
Для сумм нам нужно отметить успешные совпадения и заполнить безуспешные части великолепно гласвеевским pure Nothing
.
instance (Matching s s', Matching t t') =>
Matching (Either s t) (Either s' t') where
-- skip old stuff
match' (Left s) (Poxy :: Proxy (Either s' t')) =
((Left <$>) <$> match' s (Poxy :: Proxy s')) :*: pure Nothing
match' (Right t) (Poxy :: Proxy (Either s' t')) =
pure Nothing :*: ((Right <$>) <$> match' t (Poxy :: Proxy t'))
Для пар нам нужно собрать соответствие последовательно, выйдя раньше, если первый компонент не работает.
instance (Matching s s', Matching t t') => Matching (s, t) (s', t') where
-- skip old stuff
match' (s, t) (Poxy :: Proxy (s', t'))
= C (more <$> match' s (Poxy :: Proxy s')) where
more Nothing = pure Nothing
more (Just s) = ((,) s <$>) <$> match' t (Poxy :: Proxy t')
Итак, мы видим, что существует связь между конструктором и trie для его соединителя.
Домашнее задание: плавкий предохранитель abst
с match'
, эффективно табулирующий весь процесс.
Edit:пишу match'
, мы припарковали каждый субатчер в позиции trie, соответствующей подструктуре. И когда вы думаете о вещах в определенных позициях, вы должны думать о молниях и дифференциальном исчислении. Напомню.
Нам понадобятся функториальные константы и копродукты для управления выбором "где дыра".
data K :: * -> (* -> *) where
K :: a -> K a x
deriving (Show, Eq, Functor, Foldable, Traversable)
data (:+:) :: (* -> *) -> (* -> *) -> (* -> *) where
Inl :: f x -> (f :+: g) x
Inr :: g x -> (f :+: g) x
deriving (Show, Eq, Functor, Foldable, Traversable)
И теперь мы можем определить
class (Functor f, Functor (D f)) => Differentiable f where
type D f :: (* -> *)
plug :: (D f :*: I) x -> f x
-- there should be other methods, but plug will do for now
Применяются обычные законы исчисления, причем композиция дает пространственную интерпретацию правила цепи.
instance Differentiable (K a) where
type D (K a) = K Void
plug (K bad :*: I x) = K (absurd bad)
instance Differentiable I where
type D I = K ()
plug (K () :*: I x) = I x
instance (Differentiable f, Differentiable g) => Differentiable (f :+: g) where
type D (f :+: g) = D f :+: D g
plug (Inl f' :*: I x) = Inl (plug (f' :*: I x))
plug (Inr g' :*: I x) = Inr (plug (g' :*: I x))
instance (Differentiable f, Differentiable g) => Differentiable (f :*: g) where
type D (f :*: g) = (D f :*: g) :+: (f :*: D g)
plug (Inl (f' :*: g) :*: I x) = plug (f' :*: I x) :*: g
plug (Inr (f :*: g') :*: I x) = f :*: plug (g' :*: I x)
instance (Differentiable f, Differentiable g) => Differentiable (f :<: g) where
type D (f :<: g) = (D f :<: g) :*: D g
plug ((C f'g :*: g') :*: I x) = C (plug (f'g :*: I (plug (g' :*: I x))))
Это не повредит нам утверждать, что Expo t
дифференцируема, поэтому продолжим класс EXPO
. Что такое "три с дырой"? Это trie, в котором отсутствует выходная запись для одного из возможных входов. И это ключ.
class (Differentiable (Expo t), Applicative (Expo t)) => EXPO t where
type Expo t :: * -> *
appl :: Expo t x -> t -> x
abst :: (t -> x) -> Expo t x
hole :: t -> D (Expo t) ()
eloh :: D (Expo t) () -> t
Теперь hole
и eloh
будут свидетелями изоморфизма.
instance EXPO () where
type Expo () = I
-- skip old stuff
hole () = K ()
eloh (K ()) = ()
Случай с модулем был не очень захватывающим, но суммарный случай начинает проявлять структуру:
instance (EXPO s, EXPO t) => EXPO (Either s t) where
type Expo (Either s t) = Expo s :*: Expo t
hole (Left s) = Inl (hole s :*: pure ())
hole (Right t) = Inr (pure () :*: hole t)
eloh (Inl (f' :*: _)) = Left (eloh f')
eloh (Inr (_ :*: g')) = Right (eloh g')
См? A Left
отображается в trie с отверстием слева; a Right
отображается в trie с отверстием справа.
Теперь для продуктов.
instance (EXPO s, EXPO t) => EXPO (s, t) where
type Expo (s, t) = Expo s :<: Expo t
hole (s, t) = C (const (pure ()) <$> hole s) :*: hole t
eloh (C f' :*: g') = (eloh (const () <$> f'), eloh g')
А для пары это правая тройка, заполненная внутри левого треугольника, поэтому отверстие для определенной пары найдено путем создания отверстия для правого элемента в конкретном подтриге для левого элемента.
Для деревьев создаем другую оболочку.
newtype DExpoTree x = DExpoTree (D (Expo (Either () (Tree, Tree))) x)
deriving (Show, Eq, Functor)
Итак, как мы превращаем дерево в свой trie-распознаватель? Во-первых, мы хватаем "всех, кроме меня", и мы заполняем все эти выходы с помощью False
, затем мы вставляем True
для отсутствующей записи.
matchMe :: EXPO t => t -> Expo t Bool
matchMe t = plug ((const False <$> hole t) :*: I True)
Домашний намек: D f :*: I
- это comonad.
Отсутствуют друзья!