The core is done, just trying to elaborate 'up' to a concrete syntax.

Show thread

Trying to finalise concrete syntax for a toy imperative language. Family-styles are hard to decide from: Can the void comment on good/bad practices for concrete syntax design in this space?

re: Apreciation of Imperative Languages ;-) 

They did miss an opportunity with the name of their macro creation syntax. I feel it should have been `macros_rule !` rather than `macro_rules !` but I am not a macro fan, but I imagine those that are are a bit sad...

Show thread

Apreciation of Imperative Languages ;-) 

Learning a bit o' Rust. It seems to blend imperative and functional nicely for its design space. Not all of it I agree with but that like all languages. You like some parts, but not others. Nothing is perfect.

academic publishing politics 

PLDI is looking for comments on whether or not it should join the PACM-PL journal. (twitter.com/PLDI/status/153493). Like Sam Tobin-Hochstadt I made my comments publicly known: jfdm.github.io/statement/2022-

I’ve been blogging a bit more recently. It’s been quite good at helping me unload research thoughts out my head. I’m not too worried about the quality, more If I’m miss judging their worth. Are these things that should be followed through and written up for the beans? Not mentioning other side projects… My heart says yes, but my todos for the main research say otherwise…

**New Blog Post**: Follow the Trail! Visualising Bi-Directional Type-Checking as Network Communication.

jfdm.github.io/post/2022-06-08

@joey defining everything as Unicode and never telling you what that symbol is called or how to type is, excellent user experience /s

I have written this (using dependent types to reason about the structure of a HDL) up as a blog post.

jfdm.github.io/post/2022-05-25

I suppose this could be turned into a JFP pearl if I expand upon the other things...

Show thread

For context, for many cases `Dec : Type -> Type` is fine, but for writing interactive systems it is not. One needs `DecInfo : (e,p : Type) -> Type` to report why things failed & retain positive proof.

Show thread

Urgh, that moment when you realise ALL your predicates are not-error-message generating.

The APLAS'22 Artifact Evaluation Committee is looking for reviewers to join us in bettering the quality of research in our field.

If you want to be involved with examining state-of-the-art research then please apply!

2022.splashcon.org/track/aplas

Spread the Word!

One benefit of shifting init.el to org mode is `:tangle no`. Let's me swap out sub-configs easily. Which meant I could switch from popwin to popper; popwin wasn't popping for me.

Mastodon has a verification mechanism, though it looks different from Twitter's. We do not ask for your documents. Instead, if you have a website that you are known by, you can verify that you are the owner of that website.

Link to your Mastodon profile from the website, either through a visible link, or through a <link> tag in the head of the document, with a rel=me attribute, and link back to that page from your Mastodon profile. It should then get a green checkmark, like @Mastodon.

Finally, added the Soundness Check to an orchestration language of mine. Tempting as it is to go for the proof, working with graphs is not my forte.

/me ponders how much of a pattern this is:

```
data Tag : (this,that : Type)
-> (val : that)
-> Type
where
T : (thisVal : thisTy)
-> Tag thisTy thatTy thatVal
```

It sits between a pair and dependent pair. There is a pairing of two unrelated values...

Show older
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.