Skip to content

Commit

Permalink
use exists in BuildLibrary example
Browse files Browse the repository at this point in the history
  • Loading branch information
johnynek committed Nov 23, 2023
1 parent 8bcc02d commit b418a5c
Showing 1 changed file with 4 additions and 8 deletions.
12 changes: 4 additions & 8 deletions test_workspace/BuildLibrary.bosatsu
Original file line number Diff line number Diff line change
Expand Up @@ -5,25 +5,21 @@ export File(), Library(), LibArgs(), build, Build, file, files, build_all, libra
struct Leibniz[a, b](cast: forall f: * -> *. f[a] -> f[b])
(refl: forall a. Leibniz[a, a]) = Leibniz(x -> x)

# In Bosatsu, like System F, the type exists a. P can be encoded as forall b. (forall a. P -> b) -> b
# We encode Mapped in this way, we want: Mapped(to_tuple: exists b. (Build[b], b -> a))
# we write: Mapped(to_tuple: forall c. (forall b. (Build[b], b -> a) -> c) -> c)

struct File(path: String)
struct Library

enum Build[a]:
LoadFile(name: String, is_file: Leibniz[a, File])
Pure(value: a)
Mapped(consume: forall b. (forall c. (Build[c], c -> a) -> b) -> b)
Map2(consume: forall b. (forall c, d. (Build[c], Build[d], (c, d) -> a) -> b) -> b)
Mapped(consume: exists b. (Build[b], b -> a))
Map2(consume: exists b, c. (Build[b], Build[c], (b, c) -> a))
BuildLib(files: Build[List[File]], deps: Build[List[Library]], is_lib: Leibniz[a, Library])

def map_Build(b: Build[a], fn: a -> b) -> Build[b]:
Mapped(cb -> cb(b, fn))
Mapped((b, fn))

def map2_Build(ba: Build[a], bb: Build[b], fn: (a, b) -> c) -> Build[c]:
Map2(cb -> cb(ba, bb, fn))
Map2((ba, bb, fn))

def file(s: String) -> Build[File]:
LoadFile(s, refl)
Expand Down

0 comments on commit b418a5c

Please sign in to comment.