Search code examples
haskellabstract-syntax-treegadtarrow-abstraction

Evaluation of an AST (as a GADT) with arrows as atomic values


The following program type-checks and compiles:

import Control.Arrow

data Ns = Na | Nb | Nc | Nd deriving Show

data Net a where
    Uni :: a -> Net a
    Serial :: Net a -> Net a -> Net a
    Branch :: Show a => Net a -> Net (Net a, Net a)

deriving instance Show a => Show (Net a)

eval :: (Arrow a) => Net c -> a b (Net c)
eval (Uni m) = arr (const (Uni m))
eval (Serial m n) = eval m >>> eval n
--eval (Branch m) = eval m &&& eval m

example = Serial (Serial (Uni Na) (Uni Nb)) (Serial (Uni Nc) (Uni Nd))

main = do
    putStrLn $ show (app (eval example, Na))

However, when I try to add a case for eval (Branch m), type checking bombs out. Something of type

Arrow a => a b (Net d)

is expected, but of course the way I have it is

Arrow a => a b (c',c'')

Does anyone have a suggestion for how to write eval (Branch m)?

EDIT I

In response to @sabauma comment, I think the type signature for eval will have to change, but I'm not sure what it should be.

EDIT II

Here's an example of what should happen:

branch = Branch example
app (eval branch, Na)

should give,

Uni (Uni Na,Uni Na)

This is what @sabauma 's proposal does.


Solution

  • One possibility is

    eval :: (Arrow a) => Net c -> a b (Net c)
    eval (Uni m)      = arr (const (Uni m))
    eval (Serial m n) = eval m >>> eval n
    eval (Branch m)   = (eval m &&& eval m) >>> arr Uni
    

    I don't know if this has the desired behaviour, but it typechecks and is not the trivial solution. This lets you get away without changing the type signature.