Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
wat [2016/02/11 11:01] nikolaj |
wat [2016/04/13 16:23] nikolaj |
||
|---|---|---|---|
| Line 3: | Line 3: | ||
| Here I write down some syntax ideas for **WAT - Writing And Typing**, a programming language with a dependent type system that can very easily be parsed to the standard mathematical syntax you wouldd encounter in physics papers. | Here I write down some syntax ideas for **WAT - Writing And Typing**, a programming language with a dependent type system that can very easily be parsed to the standard mathematical syntax you wouldd encounter in physics papers. | ||
| - | >In the best case, the type both makes for an interesting mathematical structure (an $\infty$-topos?) **and** is expressive enough to formalize such structures. | + | >In the best case, the type both makes for an interesting mathematical structure (an $\infty$-topos?) or embeds in one (the point is that ist semantics should be easy understandable ("easy" from my POV at least)) **and** is expressive enough to formalize such structures. |
| - | > | + | In view of using it as starting point in [[Outline]], one could first do the latter and then explain this aspect of WAT as primary semantic example. |
| - | >* In view of AoC: (in view of using it as starting point in [[Outline]]) one could first do the latter and then explain this aspect of WAT as primary semantic example. | + | |
| - | > | + | |
| - | >* In view of applications as a language: The primitive notions should be those that will surely stay at the basis the ITT Topic. As tools, I'd like to add features that implement some of the Syntetic Diff Geo (Schreiber) | + | |
| >>What's a faithful model of (to-be) WAT? | >>What's a faithful model of (to-be) WAT? | ||
| + | |||
| + | >>>You can start with almost any dependently typed language, even if parts are missing, if you label/deny using/rule out the potentially dangerous possibilites/implementations there. What's left is something simple and right. | ||
| + | |||
| + | So todo: Make a list of what you actually WANT1111!!! --> What's the smallest theory permitting a semantic model that has all the stuff I like? | ||
| === Motivation === | === Motivation === | ||
| Line 26: | Line 27: | ||
| === Thoughts and Specification === | === Thoughts and Specification === | ||
| See [[Primitive notions . WAT]] | See [[Primitive notions . WAT]] | ||
| + | |||
| + | >In view of applications as a language: The primitive notions should be those that will surely stay at the basis the ITT Topic. As tools, I'd like to add features that implement some of the Syntetic Diff Geo (Schreiber) | ||
| * The people who would have use for WAT would all know how to read and write LaTeX, but surely not a particular programming language, let alone a typed one. My first incentive is thus to have a syntax that very much like the formula-aspect of LaTeX, and write a parser to proper LaTeX on the one hand, and to an existing programming language on the other hand. Since I don't know shit about writing a type checker but still want use lambdas and study type systems, I guess I'll naturally try to parse into [[Haskell]] and (or) some dependent Variation of it. | * The people who would have use for WAT would all know how to read and write LaTeX, but surely not a particular programming language, let alone a typed one. My first incentive is thus to have a syntax that very much like the formula-aspect of LaTeX, and write a parser to proper LaTeX on the one hand, and to an existing programming language on the other hand. Since I don't know shit about writing a type checker but still want use lambdas and study type systems, I guess I'll naturally try to parse into [[Haskell]] and (or) some dependent Variation of it. | ||
