pds

Copyright	(c) Julian Grove and Aaron Steven White 2025
License	MIT
Maintainer	julian.grove@gmail.com
Safe Haskell	Safe-Inferred
Language	Haskell2010

Framework.Lambda.Terms

Description

We encode (untyped) λ-calculus, with constants, and including a definition of probabilistic programs.

Synopsis

betaDeltaNormal :: DeltaRule -> Term -> Term
betaEtaNormal :: Term -> Term
betaNormal :: Term -> Term
type Constant = Either String Double
dCon :: Double -> Term
type DeltaRule = Term -> Maybe Term
etaNormal :: Term -> Term
freeVars :: Term -> [VarName]
fresh :: [Term] -> [VarName]
sCon :: String -> Term
subst :: VarName -> Term -> Term -> Term
data Term
- = Var VarName
- | Con Constant
- | Lam VarName Term
- | App Term Term
- | TT
- | Pair Term Term
- | Pi1 Term
- | Pi2 Term
- | Return Term
- | Let VarName Term Term
(@@) :: Term -> Term -> Term
(&) :: Term -> Term -> Term

Documentation

betaDeltaNormal :: DeltaRule -> Term -> Term Source #

Beta normal forms, taking delta rules into account.

betaEtaNormal :: Term -> Term Source #

Beta-eta normal forms.

betaNormal :: Term -> Term Source #

Beta normal forms.

type Constant = Either String Double Source #

Constants are indexed by either strings or real numbers.

dCon :: Double -> Term Source #

Turn a Double into a constant.

type DeltaRule = Term -> Maybe Term Source #

The type of Delta rules.

etaNormal :: Term -> Term Source #

Eta normal forms.

freeVars :: Term -> [VarName] Source #

fresh :: [Term] -> [VarName] Source #

sCon :: String -> Term Source #

Make arbitrarily typed constants.

subst :: VarName -> Term -> Term -> Term Source #

Substitutions.

data Term Source #

Untyped λ-terms. Types are assigned separately (i.e., "extrinsically").

Constructors

Var VarName
Con Constant
Lam VarName Term
App Term Term
TT
Pair Term Term
Pi1 Term
Pi2 Term
Return Term
Let VarName Term Term

Instances

Instances details

Num Term Source #	`Num` instance for `Term`, just as a notational convenience.
Instance details Defined in Framework.Lambda.Convenience Methods (+) :: Term -> Term -> Term # (-) :: Term -> Term -> Term # (*) :: Term -> Term -> Term # negate :: Term -> Term # abs :: Term -> Term # signum :: Term -> Term # fromInteger :: Integer -> Term #
Show Term Source #
Instance details Defined in Framework.Lambda.Terms Methods showsPrec :: Int -> Term -> ShowS # show :: Term -> String # showList :: [Term] -> ShowS #
Eq Term Source #
Instance details Defined in Framework.Lambda.Terms Methods (==) :: Term -> Term -> Bool # (/=) :: Term -> Term -> Bool #

(@@) :: Term -> Term -> Term Source #

Abbreviations for application and pairing.

(&) :: Term -> Term -> Term Source #

Abbreviations for application and pairing.