-
Notifications
You must be signed in to change notification settings - Fork 10
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Continue Updating Claro Docs to Use Auto-Validated Examples
- Loading branch information
1 parent
88ce4dd
commit 3f40d76
Showing
16 changed files
with
326 additions
and
2 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,51 @@ | ||
load("//mdbook_docs:docs_with_validated_examples.bzl", "doc_with_validated_examples") | ||
|
||
exports_files(glob(["*.claro"]), visibility = ["//mdbook_docs/src/generics/contracts/implementing_contracts:__pkg__"]) | ||
|
||
doc_with_validated_examples( | ||
name = "dynamic_dispatch", | ||
doc_template = "dynamic_dispatch.tmpl.md", | ||
examples = [ | ||
"ex1_concat.claro", | ||
{ | ||
"example": "ex2.java", | ||
"executable": False, | ||
"codeblock_css_class": "java", | ||
}, | ||
{ | ||
"example": "ex3.java", | ||
"executable": False, | ||
"codeblock_css_class": "java", | ||
}, | ||
"ex4_concat.claro", | ||
{ | ||
"example": "ex5.java", | ||
"executable": False, | ||
"codeblock_css_class": "java", | ||
}, | ||
{ | ||
"example": "ex6.claro", | ||
"hidden_setup": "claro_contracts_setup.claro", | ||
"append_output": False, | ||
}, | ||
{ | ||
"example": "ex7.claro", | ||
"hidden_setup": ["claro_contracts_setup.claro", "ex6.claro"], | ||
"expect_errors": True, | ||
}, | ||
{ | ||
"example": "ex8.claro", | ||
"hidden_setup": ["claro_contracts_setup.claro", "ex6.claro"], | ||
}, | ||
], | ||
) | ||
|
||
[ | ||
genrule( | ||
name = "{0}_concat".format(ex), | ||
outs = ["{0}_concat.claro".format(ex)], | ||
srcs = ["claro_contracts_setup.claro", "{0}.claro".format(ex)], | ||
cmd = "cat $(location {0}.claro) $(location claro_contracts_setup.claro) > $(OUTS)".format(ex), | ||
) | ||
for ex in ["ex1", "ex4"] | ||
] |
29 changes: 29 additions & 0 deletions
29
mdbook_docs/src/generics/contracts/dynamic_dispatch/claro_contracts_setup.claro
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,29 @@ | ||
|
||
$$ | ||
$$contract Stringify<T> { | ||
$$ function displayStr(t: T) -> string; | ||
$$} | ||
$$ | ||
$$newtype Foo : int | ||
$$implement Stringify<Foo> { | ||
$$ function displayStr(t: Foo) -> string { | ||
$$ var boundingLine = strings::repeated("*", len("{unwrap(t)}") + len("* Foo() *")); | ||
$$ return "{boundingLine}\n* {t} *\n{boundingLine}"; | ||
$$ } | ||
$$} | ||
$$ | ||
$$newtype Bar : string | ||
$$implement Stringify<Bar> { | ||
$$ function displayStr(t: Bar) -> string { | ||
$$ var boundingLine = strings::repeated("-", len(unwrap(t)) + len("| Bar() |")); | ||
$$ return "{boundingLine}\n| {t} |\n{boundingLine}"; | ||
$$ } | ||
$$} | ||
$$ | ||
$$newtype Buzz : string | ||
$$implement Stringify<Buzz> { | ||
$$ function displayStr(t: Buzz) -> string { | ||
$$ var boundingLine = strings::repeated("#", len(unwrap(t)) + len("# Buzz() #")); | ||
$$ return "{boundingLine}\n# {t} #\n{boundingLine}"; | ||
$$ } | ||
$$} |
104 changes: 104 additions & 0 deletions
104
mdbook_docs/src/generics/contracts/dynamic_dispatch/dynamic_dispatch.tmpl.md
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,104 @@ | ||
# Dynamic Dispatch | ||
|
||
"Dynamic Dispatch" is a fancy term for a call to an overloaded procedure (one with multiple implementations whose | ||
signatures differ only in the types of args/return value) being routed (a.k.a. "dispatched") to the appropriate | ||
implementation **based on type information solely available at runtime**. | ||
|
||
## TLDR; | ||
|
||
The short version of this section is that Claro supports the following: | ||
|
||
{{EX1}} | ||
|
||
_Feel free to ponder how this works. But keep reading if it's not immediately obvious what's going on here._ | ||
|
||
## By Comparison to Object-Oriented Programming | ||
|
||
<div class="warning"> | ||
<b>This entire section is intended to build up your intuition for Claro's approach to Dynamic Dispatch by comparing and | ||
contrasting with Java.</b> | ||
|
||
[Skip ahead TODO(steving) Add link](#dynamic-dispatch) if you're already familiar with the concept of Dynamic Dispatch, | ||
or keep reading for something of a deep dive. | ||
</div> | ||
|
||
Claro is truly a procedural language, and so is philosophically opposed to the personification of data that is a | ||
fundamental property of "Object-Oriented" programming (OOP) languages like Java/Python/C++/etc. So, you won't find | ||
anything resembling "Objects" or "Classes" in Claro. Additionally, Claro is philosophically opposed to the complexity of | ||
inheritance, so again Claro's type system does not support it. | ||
|
||
However, though Claro takes issue with the path OOP takes to achieve it, the paradigm provides some obviously useful | ||
abstractions that help programmers write very expressive code. Of particular interest in this section is the ability to | ||
write code that treats values of distinct types _interchangeably_ for the sake of dispatching to procedures that are | ||
known to be implemented over each of the distinct types in question. | ||
|
||
In a language like Java, you'll accomplish this either by using _interfaces_, or by creating _subtype relationships | ||
between types using inheritance_. | ||
|
||
### Using an Interface "Type" as a Procedure Arg (_in an OOP language_) | ||
|
||
For example, the below **Java** code defines an interface with a single "method" that three classes implement. | ||
|
||
{{EX2}} | ||
|
||
And so a **Java** programmer can write a method that accepts an argument of type `Stringify`... but in **Java** parlance | ||
any type that _implements_ the `Stringify` interface can be considered a **subtype** of `Stringify` and passed in its | ||
place: | ||
|
||
{{EX3}} | ||
|
||
This is a very convenient abstraction. However, in Java this **single** method implementation must handle multiple | ||
possible concrete subtypes of `Stringify` (in this case `Foo`, `Bar`, and `Buzz`). Java addresses this by dispatching to | ||
the correct implementation of the `displayStr()` method **at runtime**, by dynamically checking the actual concrete type | ||
of the object currently being handled. **This is already an example of Dynamic Dispatch. In Java, Dynamic Dispatch | ||
is the norm**. | ||
|
||
### Requiring a Contract to Be Implemented Over Generic Type Params (In Claro) | ||
|
||
But subtyping is by no means essential for this to be possible. By now you've already seen that | ||
[Contracts](../contracts.generated_docs.md) provide a mechanism to express the same thing without resorting to creating | ||
any subtyping relationships between types. | ||
|
||
{{EX4}} | ||
|
||
And additionally, as Claro's | ||
[generic procedures are "monomorphized"](../implementing_contracts/implementing_contracts.generated_docs.md#a-note-on-static-dispatch-via-monomorphization), | ||
there is actually **no Dynamic Dispatch going on in the above example**. And when you stop and think about it, why would | ||
there be? As a human looking at the three calls to `prettyPrint(...)`, there's zero uncertainty of the types in | ||
question. Unlike in the Java case, the Claro compiler actually takes advantage of this type information as well to | ||
generate code that **statically dispatches** to the correct implementations without requiring any runtime type checks. | ||
|
||
### A (Not So) Brief Aside on the Limitations of Subtyping | ||
|
||
You may be thinking that Java's use of subtyping makes the language simpler because it allows you to avoid the use of | ||
Generics, but this is debatable at best. Consider a very slightly modified version of the above `prettyPrint()` function | ||
that instead takes two arguments: | ||
|
||
{{EX5}} | ||
|
||
As it's currently defined, there's nothing requiring the two arguments to *actually* have the same type. In this trivial | ||
example, that may be fine, but if I were to actually want to ensure that two arguments both implement an interface | ||
**_and_** they both actually have the same type, then I'm out of luck - **there's no way to statically encode this | ||
constraint in Java!** | ||
|
||
In Claro, you would simply write: | ||
|
||
{{EX6}} | ||
|
||
And it will be a compilation error to pass arguments of different types: | ||
|
||
{{EX7}} | ||
|
||
But yet it will still be completely valid to pass arguments of the same type just like we wanted: | ||
|
||
{{EX8}} | ||
|
||
<div class="warning"> | ||
|
||
**HOT TAKE:** While Java's support for subtyping may **_seem_** like a powerful tool (and sometimes it really is | ||
convenient), it's actually explicitly **_taking away type information_**. You in fact end up with a | ||
**_less expressive_** language as a result of depending on subtyping. | ||
</div> | ||
|
||
|
||
# TODO(steving) FINISH THIS SECTION...NEED TO LAND THE PLANE AND ACTUALLY BUILD UP TO DYNAMIC DISPATCH IN CLARO |
9 changes: 9 additions & 0 deletions
9
mdbook_docs/src/generics/contracts/dynamic_dispatch/ex1.claro
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,9 @@ | ||
requires(Stringify<T>) | ||
consumer prettyPrintList<T>(l: [T]) { | ||
for (e in l) { | ||
print(Stringify::displayStr(e)); | ||
} | ||
} | ||
|
||
var elems: [oneof<Foo, Bar, Buzz>] = [Foo(1234), Bar("some string"), Buzz("another")]; | ||
prettyPrintList(elems); |
15 changes: 15 additions & 0 deletions
15
mdbook_docs/src/generics/contracts/dynamic_dispatch/ex10.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,15 @@ | ||
public class Demo { | ||
public static void main(String... args) { | ||
ArrayList<Stringify> elems = new ArrayList<>(); | ||
elems.add(new Foo(1234)); | ||
elems.add(new Bar("some string")); | ||
elems.add(new Buzz("another")); | ||
prettyPrintList(elems); | ||
} | ||
|
||
static void prettyPrintList(ArrayList<Stringify> l) { | ||
for (Stringify e : l) { | ||
System.out.println(e.displayStr()); | ||
} | ||
} | ||
} |
64 changes: 64 additions & 0 deletions
64
mdbook_docs/src/generics/contracts/dynamic_dispatch/ex2.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,64 @@ | ||
/*** JAVA ***/ | ||
$$import java.util.List; | ||
$$import java.util.ArrayList; | ||
$$import java.lang.StringBuilder; | ||
$$ | ||
interface Stringify { | ||
String displayStr(); | ||
} | ||
$$ | ||
class Foo implements Stringify { | ||
// ... | ||
$$ private final int wrapped; | ||
$$ public Foo(int wrapped) { | ||
$$ this.wrapped = wrapped; | ||
$$ } | ||
$$ | ||
@Override | ||
public String displayStr() { | ||
// ... | ||
$$ String boundingLine = Util.repeated('*', String.valueOf(this.wrapped).length() + "* Foo() *".length()); | ||
$$ return String.format("%s\n* Foo(%s) *\n%s", boundingLine, this.wrapped, boundingLine); | ||
} | ||
} | ||
$$ | ||
class Bar implements Stringify { | ||
// ... | ||
$$ private final String wrapped; | ||
$$ public Bar(String wrapped) { | ||
$$ this.wrapped = wrapped; | ||
$$ } | ||
$$ | ||
@Override | ||
public String displayStr() { | ||
// ... | ||
$$ String boundingLine = Util.repeated('-', this.wrapped.length() + "| Bar() |".length()); | ||
$$ return String.format("%s\n| Foo(%s) |\n%s", boundingLine, this.wrapped, boundingLine); | ||
} | ||
} | ||
$$ | ||
class Buzz implements Stringify { | ||
// ... | ||
$$ private final String wrapped; | ||
$$ public Buzz(String wrapped) { | ||
$$ this.wrapped = wrapped; | ||
$$ } | ||
$$ | ||
@Override | ||
public String displayStr() { | ||
// ... | ||
$$ String boundingLine = Util.repeated('#', this.wrapped.length() + "# Buzz() #".length()); | ||
$$ return String.format("%s\n# Buzz(%s) #\n%s", boundingLine, this.wrapped, boundingLine); | ||
} | ||
} | ||
$$ | ||
$$class Util { | ||
$$ public static String repeated(char c, int n) { | ||
$$ StringBuilder sb = new StringBuilder(); | ||
$$ for (; n > 0; n--) { | ||
$$ sb.append(c); | ||
$$ } | ||
$$ return sb.toString(); | ||
$$ } | ||
$$} | ||
$$ |
13 changes: 13 additions & 0 deletions
13
mdbook_docs/src/generics/contracts/dynamic_dispatch/ex3.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,13 @@ | ||
/*** JAVA ***/ | ||
public class Demo { | ||
public static void main(String... args) { | ||
// Foo, Bar, and Buzz are all "subtypes" of Stringify. | ||
prettyPrint(new Foo(1234)); | ||
prettyPrint(new Bar("some string")); | ||
prettyPrint(new Buzz("another")); | ||
} | ||
|
||
static void prettyPrint(Stringify x) { | ||
System.out.println(x.displayStr()); | ||
} | ||
} |
9 changes: 9 additions & 0 deletions
9
mdbook_docs/src/generics/contracts/dynamic_dispatch/ex4.claro
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,9 @@ | ||
#### CLARO #### | ||
prettyPrint(Foo(1234)); | ||
prettyPrint(Bar("some string")); | ||
prettyPrint(Buzz("another")); | ||
|
||
requires(Stringify<T>) | ||
consumer prettyPrint<T>(t: T) { | ||
print(Stringify::displayStr(t)); | ||
} |
13 changes: 13 additions & 0 deletions
13
mdbook_docs/src/generics/contracts/dynamic_dispatch/ex5.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,13 @@ | ||
/*** JAVA ***/ | ||
public class Demo { | ||
public static void main(String... args) { | ||
// Java allows **both** of these calls - whether you want this or not. | ||
prettyPrintPair(new Foo(1234), new Foo(56678)); | ||
prettyPrintPair(new Foo(1234), new Bar("some string")); | ||
} | ||
|
||
static void prettyPrintPair(Stringify x, Stringify y) { | ||
System.out.println("First:" + x.displayStr()); | ||
System.out.println("Second:" + x.displayStr()); | ||
} | ||
} |
6 changes: 6 additions & 0 deletions
6
mdbook_docs/src/generics/contracts/dynamic_dispatch/ex6.claro
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
#### CLARO #### | ||
requires(Stringify<T>) | ||
consumer prettyPrintPair<T>(x: T, y: T) { | ||
print("First:\n{Stringify::displayStr(x)}"); | ||
print("Second:\n{Stringify::displayStr(y)}"); | ||
} |
2 changes: 2 additions & 0 deletions
2
mdbook_docs/src/generics/contracts/dynamic_dispatch/ex7.claro
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,2 @@ | ||
#### CLARO #### | ||
prettyPrintPair(Foo(1234), Bar("some string")); |
4 changes: 4 additions & 0 deletions
4
mdbook_docs/src/generics/contracts/dynamic_dispatch/ex8.claro
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,4 @@ | ||
#### CLARO #### | ||
prettyPrintPair(Foo(1234), Foo(5678)); | ||
print(""); | ||
prettyPrintPair(Bar("some string"), Bar("another")); |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters