Хорошая печать с бесплатными монадами и GADT

Рассмотрим функтор выражения, определенный следующим GADT:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}

import Control.Monad.Free

data ExprF :: * -> * where
  Term :: Foo a -> (a -> r) -> ExprF r

instance Functor ExprF where
  fmap f (Term d k) = Term d (f . k)

type Expr = Free ExprF

где Foo определяется как

data Foo :: * -> * where
  Bar :: Int    -> Foo Int
  Baz :: Double -> Foo Double

instance Show a => Show (Foo a) where
  show (Bar j) = show j
  show (Baz j) = show j

Комбинация поля (a -> r) в ExprF и (в противном случае желательно) ограничительных конструкторов GADT, похоже, делает невозможным создание красивого интерпретатора печати:

pretty (Pure r)          = show r
pretty (Free (Term f k)) = "Term " ++ show f ++ pretty (k _)

Типовое отверстие - это то, что можно было бы ожидать:

Found hole ‘_’ with type: a1
Where: ‘a1’ is a rigid type variable bound by
            a pattern with constructor
              Term :: forall r a. Foo a -> (a -> r) -> ExprF r,
            in an equation for ‘pretty’
            at Test.hs:23:15
Relevant bindings include
  k :: a1 -> Free ExprF a (bound at Test.hs:23:22)
  f :: Foo a1 (bound at Test.hs:23:20)
  pretty :: Free ExprF a -> String (bound at Test.hs:22:1)
In the first argument of ‘k’, namely ‘_’
In the first argument of ‘pretty’, namely ‘(k _)’
In the second argument of ‘(++)’, namely ‘pretty (k _)’

Кажется, нет способа присвоить продолжению значение того типа, который ему нужен. Этот тип закодирован в f, и в других интерпретаторах я как-то использую весь дескриптор f, чтобы извлечь значение соответствующего типа. Но путь к String представлению кажется заблокированным.

Есть ли какая-то общая идиома, которую я здесь упускаю? Как можно красиво напечатать значение Expr, если это действительно возможно? Если это невозможно, какая альтернативная конструкция ExprF может фиксировать ту же структуру, но также поддерживать красивый принтер?


haskell pretty-print free-monad gadt
person jtobin    schedule 05.04.2015    source источник

Ответы (2)


arrow_upward
4
arrow_downward

Просто совпадение с образцом на f. Если вы это сделаете, тип k будет уточнен, чтобы соответствовать типу, содержащемуся внутри Foo:

pretty (Pure r)          = show r
pretty (Free (Term f k)) = "Term " ++ show f ++ pretty r where
  r = case f of
    Bar a -> k a
    Baz a -> k a

Вы можете выделить этот шаблон:

applyToFoo :: (a -> r) -> Foo a -> r
applyToFoo f (Bar a) = f a
applyToFoo f (Baz a) = f a

pretty (Pure r)          = show r
pretty (Free (Term f k)) = "Term " ++ show f ++ pretty (applyToFoo k f)
person András Kovács    schedule 05.04.2015
comment
Вы не можете сопоставить шаблон в GADT в операторе case - слишком сложно набрать. - person luqui; 05.04.2015
comment
Я могу здесь. GHC 7.8.4 и GHC 7.10.1 проверяют это без проблем. - person András Kovács; 05.04.2015
comment
Спасибо. Я приму этот ответ только потому, что он первым ударил. - person jtobin; 05.04.2015
comment
Андрас, о боже, я показываю свое несоответствие. Пора обновить, я думаю - person luqui; 05.04.2015
comment
@luqui Я почти уверен, что вы всегда могли сопоставить GADT с образцом в case выражении - это let выражения, которые заставляют GHC выдавать забавные сообщения о взрыве его мозга. - person Carl; 05.04.2015

arrow_upward
2
arrow_downward

Что ж, это не невозможно. По крайней мере, вы можете сопоставить с шаблоном f:

pretty :: (Show a) => Expr a -> String
pretty (Pure r) = show r
pretty (Free (Term f@(Bar x) k)) = "Term " ++ show f ++ pretty (k x)
pretty (Free (Term f@(Baz x) k)) = "Term " ++ show f ++ pretty (k x)

Но это не очень приятно, поскольку вы уже сделали это в экземпляре Foo show.

Таким образом, задача состоит в том, чтобы абстрагироваться надлежащим образом.

person luqui    schedule 05.04.2015
comment
/ меня качает головой. Одна из тех ночей. Спасибо. - person jtobin; 05.04.2015