Дубликатор-переводчик с HOAS

В разделе 2.3 эти действительно замечательные заметки о безусловных окончательных интерпретаторах для DSL, Олег Киселев показывает, как решить проблему разбора сериализованной DSL выражение один раз и интерпретирует его несколько раз.

Вкратце, он показывает, что "поддельный полиморфизм первого класса" с типами

newtype Wrapped = Wrapped (∀ repr. ExpSYM repr ⇒ repr)
fromTree :: String → Either ErrMsg Wrapped

не является удовлетворительным, потому что он не расширяем: для каждого набора ограничений на repr мы должны иметь разные Wrapper/fromTree. Таким образом, я склонен использовать его решение интерпретатора дубликатора. Этот вопрос касается использования этого интерпретатора с помощью HOAS.

В частности, рассмотрите следующий язык для привязок к целевому языку:

class Lam repr where
  lam :: (repr a -> repr b) -> repr (a -> b)
  app :: repr (a -> b) -> repr a -> repr b

У меня возникли проблемы с предоставлением звукового экземпляра класса Lam для моего интерпретатора duplicator. Вот что у меня есть:

data Dup repr1 repr2 a = Dup {unDupA :: repr1 a, unDupB :: repr2 a}

instance (Lam repr1, Lam repr2) => Lam (Dup repr1 repr2) where
  lam f = Dup (lam $ unDupA . f . flip Dup undefined) (lam $ unDupB . f . Dup undefined)
  app (Dup fa fb) (Dup a b) = Dup (app fa a) (app fb b)

Есть ли способ дать рекурсивный экземпляр Lambda для чего-то вроде моего типа Dup, который не включает undefined?

Я также попытался использовать более мощную версию Lam из этой статьи, которая позволяет монадическим переводчикам с помощью HOAS, хотя я и сделал Посмотрите, как это поможет мне с моим экземпляром для Dup. Решение с использованием любой версии Lam с HOAS было бы здорово!

_{*: Олег показал, как определить звуковой экземпляр, используя индексы Bruijn, но меня действительно интересует решение для HOAS.Суб >}

_{class Lam repr where
      lam :: repr (a,g) b -> repr g (a -> b)
      app :: repr g (a->b) -> repr g a -> repr g b

    data Dup repr1 repr2 g a = Dup{d1:: repr1 g a, d2:: repr2 g a}

    instance (Lam repr1, Lam repr2) => Lam (Dup repr1 repr2) where
      lam (Dup e1 e2) = Dup (lam e1) (lam e2)
      app (Dup f1 f2) (Dup x1 x2) = Dup (app f1 x1) (app f2 x2)}

Ответ 1

Это невозможно.

Чтобы показать пример, я сначала сделаю очень простой экземпляр Lam:

newtype Id a = Id a

instance Lam Id where
    lam (Id f) = Id (\x -> let Id r = f x in r)
    app (Id f) (Id x) = Id (f x)

Теперь я создам функцию, которая работает на Dup s:

f :: Dup Id Id Int -> Dup Id Id Int
f (Dup (Id x) (Id y)) = Dup (Id x*y) (Id y)

Я мог бы с экземпляра Lam выполнить lam f :: Dup Id Id (Int -> Int). Это может выглядеть как

Dup (Id (\x -> x*y)) (Id (\y -> y))

который невозможно сделать, потому что y недоступен из x -lambda. (Использование undefined заменяет y на undefined здесь, бросая ошибки во время выполнения, когда это не работает хорошо). Это не редкость: это происходит в любой момент, когда вы используете одну из переменных в другом результате.

Я не уверен, что вы спрашиваете с более сильным Monad -общим обобщением, но это происходит и с другими Monad s: например, с Maybe, вы не можете следуя за Maybe (Int -> Int), потому что это зависит от заданного значения:

f :: Maybe Int -> Maybe Int
f m = m >>= \x -> if x > 5 then Just x else Nothing

(Вы можете использовать fromJust на нем и надеяться, что никто этого не сделает, но он так же, как и решение undefined.)

undefined выдает ошибку только в том случае, если функция должна смотреть на другие переменные. Если вы абсолютно уверены, что он никогда не будет запущен ни на что подобное, (например, вы ограничиваете развертывание/создание в тщательно проверенном скрытом модуле), тогда будет работать undefined.

Еще одна рекомендация: используйте более подробное error сообщение вместо undefined, если что-то пойдет не так.

Ответ 2

После некоторой работы с Template Haskell у меня появилась идея, которая применима здесь. Другим вариантом было бы сделать это так, как это делает TH:

class Fail.MonadFail m => Quasi m where
    -- All the things here, like inspecting types, generating names, etc.
    ...

-- Many instances, including
instance Quasi IO where ... -- So you can debug your TH
instance TH.Quasi GHCiQ where ... -- see https://github.com/ghc/ghc/blob/master/libraries/ghci/GHCi/TH.hs#L167
instance TH.Quasi TcM where ... -- see https://github.com/ghc/ghc/blob/master/compiler/typecheck/TcSplice.hs#L835

data Q a = { unQ :: forall m. Quasi m => m a }
instance Quasi Q where ...

Вы можете найти определение монады Q здесь.

Конечный пользователь работает в монаде Q, и его можно интерпретировать любым внутренним интерпретатором компилятора или монадой IO для отладки и т.д. Любое дублирование обрабатывается forall. Аналогичным образом вы могли бы сделать что-то вроде

data L a = { unL :: forall repr. Lam repr => repr a }
instance Lam L where ...

myEndUserThing :: L ((a -> b) -> a -> b)
myEndUserThing = lam $ \f -> lam $ \x -> app f x

L a легко конвертируется в любой другой repr, который вам нужен, и если вам нужно больше функциональности, просто добавьте его в класс Lam или создайте класс вывода с дополнительными функциями.