Skip to content

Commit 5d3d400

Browse files
kztk-mkztk-m
committed
Merge remote-tracking branch 'ebu-examples/to_merge'
2 parents 3df7d97 + bb3408d commit 5d3d400

File tree

9 files changed

+2096
-0
lines changed

9 files changed

+2096
-0
lines changed

‎ebu-examples/LICENSE‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
Copyright (c) 2023, 2024 Kazutaka Matsuda, and Samantha Frohlich
2+
3+
All rights reserved.
4+
5+
Redistribution and use in source and binary forms, with or without
6+
modification, are permitted provided that the following conditions are met:
7+
8+
* Redistributions of source code must retain the above copyright
9+
notice, this list of conditions and the following disclaimer.
10+
11+
* Redistributions in binary form must reproduce the above
12+
copyright notice, this list of conditions and the following
13+
disclaimer in the documentation and/or other materials provided
14+
with the distribution.
15+
16+
* Neither the name of the copyright holder nor the names of other
17+
contributors may be used to endorse or promote products derived
18+
from this software without specific prior written permission.
19+
20+
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
21+
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
22+
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
23+
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
24+
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
25+
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
26+
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
27+
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
28+
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
29+
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
30+
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

‎ebu-examples/README.md‎

Lines changed: 92 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,92 @@
1+
Examples for Embedding by Unembedding
2+
=====================================
3+
4+
This is a collection of proof-of-concept application examples of the [embedding-by-unembedding](https://github.com/kztk-m/EbU).
5+
6+
* `AppLens.hs` - extracts of code for a simple lens language from the ["Embedding by Unembedding" paper](https://doi.org/10.1145/3607830).
7+
* `CTS.hs` - the cache transfer variant of the incremental lambda calculus.
8+
* `ELens.hs` - bidirectional transformations
9+
* `STLC.hs` - example usage of the framework on the simply typed lambda calc. (This is a good file to start in to understand the Embedding by Unembedding technique)
10+
* `ILC.hs` - the incremental lambda calculus (<https://inc-lc.github.io/>)
11+
12+
The code is supposed to be used in REPL, by:
13+
14+
```
15+
cabal repl
16+
```
17+
18+
Then, as shown below, you can experiment with code in each of the files by focussing on them with `:l`.
19+
20+
Usage Examples: `ELens.hs`
21+
--------------------------
22+
23+
```haskell
24+
$ cabal repl
25+
ghci> :l Unembedding.Examples.ELens
26+
[1 of 1] Compiling Unembedding.Examples.ELens
27+
Ok, one module loaded.
28+
ghci> :t linesB
29+
linesB :: HOBiT e => e String -> e [String]
30+
ghci> :t runHOBiT linesB
31+
runHOBiT linesB :: Lens String [String]
32+
ghci> let l = runHOBiT linesB
33+
ghci> :t l
34+
l :: Lens String [String]
35+
ghci> get l "A\nB"
36+
Right ["A","B"]
37+
ghci> put l "A\nB" ["a","b"]
38+
Right "a\nb"
39+
ghci> put l "A\nB" ["a","b","c"]
40+
Right "a\nb\nc"
41+
ghci> put l "A\nB" ["a"]
42+
Right "a"
43+
ghci> get l "A\nB\n"
44+
Right ["A","B"]
45+
ghci> put l "A\nB\n" ["a", "b"]
46+
Right "a\nb\n"
47+
ghci> put l "A\nB\n" ["a", "b", "c"]
48+
Right "a\nb\nc\n"
49+
ghci> put l "A\nB\n" ["a"]
50+
Right "a\n"
51+
```
52+
53+
Usage Examples: `CTS.hs`
54+
------------------------
55+
56+
```haskell
57+
$ cabal repl
58+
ghci> :l Unembedding.Examples.CTS
59+
[1 of 1] Compiling Unembedding.Examples.CTS
60+
Ok, one module loaded.
61+
ghci> :t cartesianRecreation
62+
cartesianRecreation
63+
:: (CTSSeq exp, Diff a, Diff b) =>
64+
exp (Seq a) -> exp (Seq b) -> exp (Seq (a, b))
65+
ghci>
66+
ghci> :t runCTS
67+
runCTS
68+
:: Diff a => CTS '[a] b -> a -> (b, Interact (Delta a) (Delta b))
69+
ghci> :t UE.runOpen (\z -> cartesianRecreation (fst_ z) (snd_ z))
70+
UE.runOpen (\z -> cartesianRecreation (fst_ z) (snd_ z))
71+
:: (Variables sem, CTSSeq (EnvI sem), Diff a, Diff b) =>
72+
sem '[(Seq a, Seq b)] (Seq (a, b))
73+
ghci> :t caInc
74+
caInc
75+
:: (Diff a, Diff b) =>
76+
(Seq a, Seq b)
77+
-> (Seq (a, b),
78+
Interact (Delta (Seq a, Seq b)) (Delta (Seq (a, b))))
79+
ghci> let (res, i) = caInc (S.fromList [1,2,3::Int], S.fromList [4,5,6::Int])
80+
ghci> res
81+
fromList [(1,4),(1,5),(1,6),(2,4),(2,5),(2,6),(3,4),(3,5),(3,6)]
82+
ghci> let (db1, i1) = runInteract i (PairDelta (DSeq [Ins 0 42]) mempty)
83+
ghci> db1
84+
DSeq [Ins 0 (42,6),Ins 0 (42,5),Ins 0 (42,4)]
85+
ghci> res /+ db1
86+
fromList [(42,4),(42,5),(42,6),(1,4),(1,5),(1,6),(2,4),(2,5),(2,6),(3,4),(3,5),(3,6)]
87+
ghci> let (db1', i1') = runInteract i (PairDelta mempty (DSeq [Ins 0 42]))
88+
ghci> db1'
89+
DSeq [Ins 0 (1,42),Ins 4 (2,42),Ins 8 (3,42)]
90+
ghci> res /+ db1'
91+
fromList [(1,42),(1,4),(1,5),(1,6),(2,42),(2,4),(2,5),(2,6),(3,42),(3,4),(3,5),(3,6)]
92+
```

‎ebu-examples/embedding-by-unembedding-examples.cabal‎

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
cabal-version: 2.4
2+
name: embedding-by-unembedding-examples
3+
version: 0.6.0
4+
5+
license: BSD-3-Clause
6+
author: Kazutaka Matsuda, Samantha Frohlich
7+
maintainer: kztk@tohoku.ac.jp
8+
9+
common deps
10+
build-depends:
11+
base >= 4.12 && < 5,
12+
mtl ^>= 2.2 || ^>= 2.3,
13+
containers ^>= 0.6,
14+
embedding-by-unembedding ^>= 0.6 || ^>=0.7,
15+
defun-core
16+
17+
default-language: Haskell2010
18+
ghc-options:
19+
-Wall
20+
-Wcompat
21+
-Widentities
22+
-Wincomplete-uni-patterns
23+
-Wincomplete-record-updates
24+
-Wredundant-constraints
25+
-Wnoncanonical-monad-instances
26+
if impl(ghc >= 8.2)
27+
ghc-options: -fhide-source-paths
28+
if impl(ghc >= 8.4)
29+
ghc-options: -Wmissing-export-lists
30+
-Wpartial-fields
31+
if impl(ghc >= 8.8)
32+
ghc-options: -Wmissing-deriving-strategies
33+
-fwrite-ide-info
34+
-hiedir=.hie
35+
if impl(ghc >= 8.10)
36+
ghc-options: -Wunused-packages
37+
38+
library
39+
import: deps
40+
exposed-modules:
41+
Unembedding.Examples.AppLens
42+
Unembedding.Examples.CTS
43+
Unembedding.Examples.ELens
44+
Unembedding.Examples.ILC
45+
Unembedding.Examples.STLC
46+
Unembedding.Examples.Forall
47+
48+
hs-source-dirs: src
49+
default-language: Haskell2010

‎ebu-examples/src/Unembedding/Examples/AppLens.hs‎

Lines changed: 114 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,114 @@
1+
{-
2+
3+
Lens code for paper
4+
5+
-}
6+
7+
{-# LANGUAGE ConstraintKinds #-}
8+
{-# LANGUAGE DataKinds #-}
9+
{-# LANGUAGE DerivingStrategies #-}
10+
{-# LANGUAGE FlexibleContexts #-}
11+
{-# LANGUAGE FlexibleInstances #-}
12+
{-# LANGUAGE FunctionalDependencies #-}
13+
{-# LANGUAGE GADTs #-}
14+
{-# LANGUAGE LambdaCase #-}
15+
{-# LANGUAGE NoMonomorphismRestriction #-}
16+
{-# LANGUAGE PatternSynonyms #-}
17+
{-# LANGUAGE PolyKinds #-}
18+
{-# LANGUAGE RankNTypes #-}
19+
{-# LANGUAGE ScopedTypeVariables #-}
20+
{-# LANGUAGE TypeApplications #-}
21+
{-# LANGUAGE TypeFamilies #-}
22+
{-# LANGUAGE TypeFamilyDependencies #-}
23+
{-# LANGUAGE TypeOperators #-}
24+
{-# LANGUAGE UndecidableInstances #-}
25+
{-# OPTIONS_GHC -Wno-missing-export-lists #-}
26+
{-# OPTIONS_GHC -Wno-unused-imports #-}
27+
{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
28+
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
29+
30+
module Unembedding.Examples.AppLens where
31+
32+
-- base
33+
import Data.Maybe (fromMaybe)
34+
import Data.Proxy (Proxy (..))
35+
import Prelude hiding (LT)
36+
37+
-- unembedding tooling
38+
import Unembedding.Env
39+
import Unembedding (Dim (..), EnvI (..), TEnv, Variables (..), ol0)
40+
import qualified Unembedding as UE
41+
42+
-- Step 1: Identity semantic domain
43+
-- -----------------------------------------------------------------------------
44+
45+
-- type
46+
newtype LensTerm env a = LT {runLT :: TEnv env -> Lens (VEnv env) a}
47+
type VEnv = Env Maybe
48+
data Lens s v = L {get :: s -> v, put :: s -> v -> s}
49+
50+
-- var instance
51+
52+
instance Variables LensTerm where
53+
var = LT $ \(ECons _ e) ->
54+
L (\(ECons (Just a) _) -> a) -- get
55+
(\_ a -> ECons (Just a) (unitEnv e)) -- put
56+
weaken t = LT $ \(ECons _ e) ->
57+
let l = runLT t e
58+
in L (\(ECons _ env) -> get l env) -- get
59+
(\(ECons b env) a -> ECons b (put l env a)) -- put
60+
61+
-- Step 2: Prepare semantic functions for each construct
62+
-- -----------------------------------------------------------------------------
63+
64+
-- the lenses do all the work, we are writing lenses over the envs, which do the shuffling
65+
-- then get packed up as terms
66+
67+
unpairSem :: LensTerm env (a, b) -> LensTerm (a ': b ': env) r -> LensTerm env r
68+
unpairSem t1 t2 = LT $ \e ->
69+
let l1 = runLT t1 e
70+
l2 = runLT t2 (ECons Proxy (ECons Proxy e))
71+
in letLens l1 (rearrPair l2)
72+
73+
rearrPair :: Lens (VEnv (a ': b ': env)) r -> Lens (VEnv ((a, b) ': env)) r
74+
rearrPair l = L g p
75+
where
76+
g (ECons (Just (a, b)) env) = get l (ECons (Just a) (ECons (Just b) env))
77+
p (ECons (Just (a, b)) env) r =
78+
let ECons m (ECons n env') = put l (ECons (Just a) (ECons (Just b) env)) r
79+
in ECons (Just (fromMaybe a m, fromMaybe b n)) env'
80+
81+
letLens :: Lens (VEnv env) a -> Lens (VEnv (a ': env)) b -> Lens (VEnv env) b
82+
letLens l1 l2 = L g p
83+
where
84+
g env = get l2 (ECons (Just (get l1 env)) env)
85+
p env b = let a = get l1 env
86+
ECons m env1' = put l2 (ECons (Just a) env) b
87+
env2' = put l1 env (fromMaybe a m)
88+
in merge env1' env2'
89+
90+
letSem :: LensTerm env a -> LensTerm (a : env) b -> LensTerm env b
91+
letSem t1 t2 = LT $ \e -> letLens (runLT t1 e) (runLT t2 (ECons Proxy e))
92+
93+
merge :: VEnv env -> VEnv env -> VEnv env
94+
merge = undefined
95+
96+
unitEnv :: TEnv env -> VEnv env
97+
unitEnv ENil = ENil
98+
unitEnv (ECons _ e) = ECons Nothing (unitEnv e)
99+
100+
-- Step 3: Provide HOAS rep of syntax
101+
-- -----------------------------------------------------------------------------
102+
103+
class AppLens exp where
104+
prim :: Lens a b -> exp a -> exp b
105+
unit :: exp ()
106+
pair :: exp a -> exp b -> exp (a,b)
107+
108+
class AppLens exp => AppLensUnpair exp where
109+
unpair :: exp (a, b) -> (exp a -> exp b -> exp r) -> exp r
110+
111+
-- Step 4: Implement HOAS functions by lifting semantic functions
112+
-- -----------------------------------------------------------------------------
113+
114+
-- instance with lifting

0 commit comments

Comments
 (0)