\x -> y -> maybePLam \x -> yA x y z -> maybePCon $ A x y zcase x of { ... } -> maybePMatch x \case { ... }
Similarly for pattern guards, and other built-in syntax that can't be overloaded.
# Class-based solution
class MaybePLam x y out | out -> x y where
maybePLam :: (x -> y) -> out
instance PLC e => MaybePLam (Term e a) (Term e b) (Term e (a #-> b)) where
maybePLam = plam
instance {-# OVERLAPPABLE #-} PLC e => MaybePLam a b (a -> b) where
maybePLam = id
# Type-family-based solution
type family F1 (x :: Type) :: Type where
F1 (Term e (a #-> b)) = Term e a
F1 (a -> b) = a
type family F2 (x :: Type) :: Type where
F2 (Term e (a #-> b)) = Term e b
F2 (a -> b) = b
type family IsTermFunc (x :: Type) :: Bool where
F2 (Term e (_ #-> _)) = 'True
F2 (a -> b) = 'False
maybePLam :: KnownBool (IsTermFunc out) => (F1 out -> F2 out) -> out
maybePLam = ...
L-as
commented
1 year ago
\x -> y->maybePLam \x -> yA x y z->maybePCon $ A x y zcase x of { ... }->maybePMatch x \case { ... }Similarly for pattern guards, and other built-in syntax that can't be overloaded.