A cunning interpreter for the pure untyped λ-calculus.
severen.dev
1-- SPDX-FileCopyrightText: 2022 Severen Redwood <sev@severen.dev>
2-- SPDX-License-Identifier: GPL-3.0-or-later
3
4module Sly.Syntax
5 ( Name (..),
6 Statement (..),
7 Term (..),
8 astShow,
9 toChurchNat,
10 fromChurchNat,
11 toChurchBool,
12 fromChurchBool,
13 )
14where
15
16import Data.String (IsString)
17import Data.String.Interpolate (i)
18import Data.Text (Text)
19import Data.Text qualified as T
20
21-- | A name in a program.
22--
23-- A name is an identifier that is either used as a variable or an identifier to which an
24-- arbitrary term is bound.
25newtype Name = Name Text deriving (Eq, Ord, Show, IsString)
26
27-- | A program statement.
28data Statement
29 = -- | A λ-term.
30 Term Term
31 | -- | An assignment of a name to a λ-term.
32 Ass {-# UNPACK #-} !Name Term
33 deriving (Eq)
34
35instance Show Statement where
36 show (Term t) = show t <> "."
37 show (Ass (Name n) t) = T.unpack [i|let #{n} := #{T.pack (show t)}.|]
38
39-- | A λ-term.
40data Term
41 = -- | A variable.
42 Var {-# UNPACK #-} !Name
43 | -- | A λ-abstraction.
44 Abs {-# UNPACK #-} !Name Term
45 | -- | An application of a λ-abstraction.
46 App Term Term
47 deriving (Eq)
48
49instance Show Term where
50 show = T.unpack . go
51 where
52 go :: Term -> Text
53 go (Var (Name n)) = n
54 go (Abs (Name n) body) = "λ" <> n <> slurp body
55 go (App l@(Abs _ _) r@(Abs _ _)) = [i|(#{go l}) (#{go r})|]
56 go (App l@(Abs _ _) r) = [i|(#{go l}) #{go r}|]
57 go (App l r@(Abs _ _)) = [i|#{go l} (#{go r})|]
58 go (App l r@(App _ _)) = [i|#{go l} (#{go r})|]
59 go (App l r) = [i|#{go l} #{go r}|]
60
61 -- Slurp up λ-abstractions!
62 slurp :: Term -> Text
63 slurp (Abs (Name n) body) = " " <> n <> slurp body
64 slurp body = " -> " <> go body
65
66-- | Like regular show, but displays the term fully bracketed.
67astShow :: Term -> String
68astShow = T.unpack . go
69 where
70 go (Var (Name n)) = n
71 go (Abs (Name n) t) = [i|(λ#{n} -> #{go t})|]
72 go (App l r) = [i|(#{go l} #{go r})|]
73
74-- | Convert a nonnegative integer into a Church numeral term.
75toChurchNat :: Int -> Term
76toChurchNat n =
77 Abs "s" $
78 Abs "z" $
79 iterate (App (Var "s")) (Var "z") !! n
80
81-- | Convert a term into a nonnegative integer if it has the shape of a Church
82-- numeral.
83fromChurchNat :: Term -> Maybe Int
84fromChurchNat (Abs f (Abs x body)) = go 0 body
85 where
86 go :: Int -> Term -> Maybe Int
87 go n = \case
88 Var y | y == x -> Just n
89 App (Var g) t | g == f -> go (n + 1) t
90 _ -> Nothing
91fromChurchNat _ = Nothing
92
93-- | Convert a Boolean into a Church Boolean term.
94toChurchBool :: Bool -> Term
95toChurchBool True = Abs "t" $ Abs "f" (Var "t")
96toChurchBool False = Abs "t" $ Abs "f" (Var "f")
97
98-- | Convert a term into a Boolean if it has the shape of a Church Boolean.
99fromChurchBool :: Term -> Maybe Bool
100fromChurchBool (Abs t (Abs f (Var x)))
101 | x == t = Just True
102 | x == f = Just False
103fromChurchBool _ = Nothing