Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

(Quasi)ABTs for syntax types #715

Merged
merged 60 commits into from
Mar 20, 2024
Merged

(Quasi)ABTs for syntax types #715

merged 60 commits into from
Mar 20, 2024

Conversation

robrix
Copy link
Contributor

@robrix robrix commented Mar 15, 2024

Props to @BekaValentine for a discussion of the advantages of the approach for typed and untyped syntax. As yet we're only employing untyped syntax, but it's looking pretty reasonable.

Comment on lines 118 to 162
instance Eq1 Python where
liftEq _ a b = case (a, b) of
(Noop', Noop') -> True
(Iff', Iff') -> True
(Bool' b1, Bool' b2) -> b1 == b2
(String' s1, String' s2) -> s1 == s2
(Throw', Throw') -> True
(Let' n1, Let' n2) -> n1 == n2
((:>>>), (:>>>)) -> True
(Import' i1, Import' i2) -> i1 == i2
(Function' n1 as1, Function' n2 as2) -> n1 == n2 && as1 == as2
(Call', Call') -> True
(ANil', ANil') -> True
(ACons', ACons') -> True
(Locate' s1, Locate' s2) -> s1 == s2
_ -> False

instance Ord1 Python where
liftCompare _ a b = case (a, b) of
(Noop', Noop') -> EQ
(Noop', _) -> LT
(Iff', Iff') -> EQ
(Iff', _) -> LT
(Bool' b1, Bool' b2) -> compare b1 b2
(Bool' _, _) -> LT
(String' s1, String' s2) -> compare s1 s2
(String' _, _) -> LT
(Throw', Throw') -> EQ
(Throw', _) -> LT
(Let' n1, Let' n2) -> compare n1 n2
(Let' _, _) -> LT
((:>>>), (:>>>)) -> EQ
((:>>>), _) -> LT
(Import' i1, Import' i2) -> compare i1 i2
(Import' _, _) -> LT
(Function' n1 as1, Function' n2 as2) -> compare n1 n2 <> compare as1 as2
(Function' _ _, _) -> LT
(Call', Call') -> EQ
(Call', _) -> LT
(ANil', ANil') -> EQ
(ANil', _) -> LT
(ACons', ACons') -> EQ
(ACons', _) -> LT
(Locate' s1, Locate' s2) -> compare s1 s2
(Locate' _, _) -> LT
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We can't derive these because GHC.Generics doesn't play well with GADTs (or the other way around, I suppose). This is substantially worse than what we'd get using standard Fix-based terms or even plain old data.

@robrix robrix marked this pull request as ready for review March 19, 2024 19:09
@robrix robrix requested a review from a team as a code owner March 19, 2024 19:09
Copy link
Contributor Author

@robrix robrix left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ready for review.

Comment on lines +17 to +20
-- | (Currently) untyped term representations.
data Term sig v
= Var v
| Term (sig (Term sig v))
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A free monad by any other name

Comment on lines +22 to +25
instance (Eq (sig (Term sig v)), Eq v) => Eq (Term sig v) where
Var v1 == Var v2 = v1 == v2
Term s1 == Term s2 = s1 == s2
_ == _ = False
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The instance head can be cleaned up (and avoid the use of UndecidableInstances) using QuantifiedConstraints. However:

  • for Ord you end up needing to supply quantified constraints for both Eq and Ord, and
  • it was causing spurious CI failures for ghc9.2 and I really can't be bothered

Comment on lines +37 to +38
foldTerm :: Functor sig => (v -> r) -> (sig r -> r) -> (Term sig v -> r)
foldTerm var sig = mendlerTerm var (\ k -> sig . fmap k)
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here be recursion schemes 🐉

@robrix robrix merged commit 3baf0b4 into main Mar 20, 2024
2 checks passed
@robrix robrix deleted the always-be-treeing branch March 20, 2024 13:16
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants