bound-simple: A lightweight implementation of 'bound'

[ bsd3, language, library ] [ Propose Tags ]

An abstraction for representing bound variables. Most of this code has been extracted from bound, with the purpose of providing a mostly self-contained library for implementing embedded languages.


[Skip to Readme]

Modules

[Index] [Quick Jump]

Downloads

Maintainer's Corner

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.1.0.0, 0.2.0.0
Change log Changelog.md
Dependencies base (>=4.7 && <5), transformers [details]
License BSD-3-Clause
Copyright 2013 Edward Kmett, 2021 Marco Zocca
Author Marco Zocca
Maintainer ocramz
Category Language
Home page https://github.com/ocramz/bound-simple
Source repo head: git clone https://github.com/ocramz/bound-simple
Uploaded by ocramz at 2021-10-18T21:48:51Z
Distributions NixOS:0.2.0.0
Downloads 126 total (5 in the last 30 days)
Rating 2.0 (votes: 1) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2021-10-18 [all 1 reports]

Readme for bound-simple-0.2.0.0

[back to package description]

bound-simple

A lightweight implementation of 'bound'. Provides much of the functionality of Bound.Scope.Simple, without the large dependency footprint.

Example

The function whnf beta-reduces a term of the untyped lambda calculus.

In the code below, we first declare a type Exp for terms, using the Scope type within the constructor for a lambda abstraction. To this we add a few instances necessary for showing and traversing the terms. The Monad instance takes care of variable substitution. After that, abstraction and application are implemented in terms of abstract1 and instantiate1. The test function declares a term (\x . x) y , then prints it and its reduced form.

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE DerivingVia #-}

import Control.Monad (ap)
import Bound.Simple (Scope, Bound(..), abstract1, instantiate1)
import Data.Functor.Classes (Show1)
import Data.Functor.Classes.Generic (Generically(..))
import GHC.Generics (Generic1)

infixl 9 :@
data Exp a = V a | Exp a :@ Exp a | Lam (Scope () Exp a)
  deriving (Show, Functor, Foldable, Traversable, Generic1)
  deriving (Show1) via Generically Exp

instance Applicative Exp where pure = V; k <*> m = ap k m

instance Monad Exp where
  return = V
  V a      >>= f = f a
  (x :@ y) >>= f = (x >>= f) :@ (y >>= f)
  Lam e    >>= f = Lam (e >>>= f)

lam :: Eq a => a -> Exp a -> Exp a
lam v b = Lam (abstract1 v b)

whnf :: Exp a -> Exp a
whnf (e1 :@ e2) = case whnf e1 of
  Lam b -> whnf (instantiate1 e2 b)
  f'    -> f' :@ e2
whnf e = e

test :: IO ()
test = do
  let term = lam x (V x) :@ V y
  print term         -- Lam (Scope (V (B ()))) :@ V y
  print $ whnf term  -- V y