{-# LANGUAGE ExistentialQuantification #-}
module PTree where
import Control.Applicative

data PTree i o =  -- oops, "in" is a keyword.
   forall t1 t2. PBin (t1 -> t2 -> o) (PTree i t1) (PTree i t2)
   | forall t. PUn (t -> o) (PTree i t)
   | PV (i -> o)

ptreeToFunc :: PTree a b -> a -> b
ptreeToFunc (PBin f l r) =  f <$> ptreeToFunc l <*> ptreeToFunc r
ptreeToFunc (PUn f u) = f.(ptreeToFunc u)
ptreeToFunc (PV f) = f

-- and a test

type In = ()
type Out = Int

data A = A Int
data B = B Int
data D = D Int
data E = E Int

bin1 (A x) (B y) = (x+y)
un1 (D x) = A (-x)
un2 (E x) = B (x+1)
v1 () = D 3
v2 () = E 2

test :: PTree In Out
test = PBin bin1 (PUn un1 (PV v1)) (PUn un2 (PV v2))

res :: Int
res = ptreeToFunc test ()

-- and another test

data R = R Int
data S = S Int

v1' () = R 3
v2' () = S 2

-- correctly does not typecheck
-- test' :: PTree In Out
-- test' = PBin bin1 (PUn un1 (PV v1')) (PUn un2 (PV v2'))

{-
PTree.hs:45:31:
    Couldn't match expected type `D' against inferred type `R'
    In the first argument of `PV', namely `v1''
    In the second argument of `PUn', namely `(PV v1')'
    In the second argument of `PBin', namely `(PUn un1 (PV v1'))'
-}