2
\$\begingroup\$

Is it possible to reify the graph of lambda terms expressed as parametric HOAS. Not quite sure if it is

data PLambda a where
   Var   ∷ a → PLambda a
   Lam   ∷ (a  → PLambda a) → PLambda a
   App   ∷ PLambda a  → PLambda a  → PLambda a

newtype Lambda = Hide { reveal ∷ ∀ a. PLambda a}


data PLambdaNode a n where
   GraphVar ∷ a → PLambdaNode a n
   GraphLam ∷ (a → PLambdaNode a n) → PLambdaNode a n
   GraphApp ∷ n → n → PLambdaNode a n

instance MuRef (PLambda a) where
  type DeRef (PLambda a) = PLambdaNode a
  mapDeRef :: Applicative f => (forall b. (MuRef b, DeRef (PLambda a) ~ DeRef b) => b -> f u) -> PLambda a -> f (PLambdaNode a u)
  mapDeRef f (Var x) = pure $ GraphVar x
  mapDeRef f (Lam l) =  let
               b = (\a → f (l a ∷ PLambda a)) -- a → f u
             in GraphLam <$> (undefined ∷ f (a → PLambdaNode a u))
  mapDeRef f (App l x) =  GraphApp  <$> f l <*> f x
\$\endgroup\$
  • \$\begingroup\$ Is this real Haskell code? Some autocorrect process seems to have prettified it. \$\endgroup\$ – 200_success Jul 1 '16 at 17:47
  • 1
    \$\begingroup\$ it is. are you referring to the unicode syntax ? (that's {-# LANGUAGE UnicodeSyntax #-} ) \$\endgroup\$ – nicolas Jul 2 '16 at 0:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.