{
"path": "/3mathyarwzm6z",
"site": "at://did:plc:s5wwr2ccjuqricdxiyiuspfv/site.standard.publication/3m7zleg5tyc2b",
"$type": "site.standard.document",
"title": "Weekly Review - Week 12",
"content": {
"$type": "pub.leaflet.content",
"pages": [
{
"id": "3mathyaruqsul",
"$type": "pub.leaflet.pages.linearDocument",
"blocks": [
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": "This post is a summary of my activities related to coding and software in the past week. Its purpose is both to serve as a high-level personal log and as a potential source of interesting (or not so interesting) links. Entries are provided in no particular order with minimal comments..."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 21,
"byteStart": 0
},
"features": [
{
"uri": "http://www.grammaticalframework.org/",
"$type": "pub.leaflet.richtext.facet#link"
}
]
}
],
"plaintext": "Grammatical Framework"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": ": A fascinating piece of work whose purpose is to provide a way to define unified grammars that can be \"linearized\" into different languages for the purpose of both parsing and text generation."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 24,
"byteStart": 0
},
"features": [
{
"uri": "https://korewanetadesu.com/emacs-on-os-x.html",
"$type": "pub.leaflet.richtext.facet#link"
}
]
}
],
"plaintext": "Emacs Daemon on Mac OS X"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 140,
"byteStart": 120
},
"features": [
{
"$type": "pub.leaflet.richtext.facet#code"
}
]
}
],
"plaintext": ": Configuration for running Emacs in server mode which is useful for fast editing of files from the command-line: Run emacsclient foo.txt& and the file's content is displayed in a buffer in emacs."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 31,
"byteStart": 0
},
"features": [
{
"uri": "https://en.wikipedia.org/wiki/Axel_Honneth",
"$type": "pub.leaflet.richtext.facet#link"
}
]
}
],
"plaintext": "La lutte pour la reconnaissance"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": ": Finished reading this book from Axel Honneth, a German philosopher heir to the Frankfurt School. Worthy of some extended blog post..."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 33,
"byteStart": 0
},
"features": [
{
"uri": "https://addons.mozilla.org/fr/firefox/addon/org-mode-capture/",
"$type": "pub.leaflet.richtext.facet#link"
}
]
}
],
"plaintext": "Capture org-mode links in Firefox"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": ": A nice utility to quickly capture links in Firefox and add them to Emacs' org-mode"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 6,
"byteStart": 0
},
"features": [
{
"uri": "https://github.com/cantino/huginn",
"$type": "pub.leaflet.richtext.facet#link"
}
]
}
],
"plaintext": "Huggin"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": ": A tool in Rails to create and manage agents on a personal server, something I have been thinking to setup for a while."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 9,
"byteStart": 0
},
"features": [
{
"uri": "https://syncthing.net/",
"$type": "pub.leaflet.richtext.facet#link"
}
]
}
],
"plaintext": "Syncthing"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": ": Open-source system to synchronize several devices"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 53,
"byteStart": 0
},
"features": [
{
"uri": "https://vimeo.com/162036084",
"$type": "pub.leaflet.richtext.facet#link"
}
]
}
],
"plaintext": "Types + Properties = Software - Mark Seemann on Vimeo"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 50,
"byteStart": 33
},
"features": [
{
"uri": "https://www.meetup.com/fr-FR/Crafting-Software/events/238241119/",
"$type": "pub.leaflet.richtext.facet#link"
}
]
},
{
"index": {
"byteEnd": 187,
"byteStart": 158
},
"features": [
{
"uri": "http://blog.ploeh.dk/2016/02/10/types-properties-software/",
"$type": "pub.leaflet.richtext.facet#link"
}
]
},
{
"index": {
"byteEnd": 347,
"byteStart": 230
},
"features": [
{
"uri": "http://mirrors.link/posts/the-polyglot-approach-to-modeling-state-and-property-tests-in-elm",
"$type": "pub.leaflet.richtext.facet#link"
}
]
}
],
"plaintext": ": While working on my talk for Crafting Software meetup, I discovered previous work from Mark Seeman in the same vein. There is a whole blog post series on Types + Properties = Software which is definitely interesting. Inspired The Polyglot Approach to Getting Better at Modeling the State and Writing Property Tests in Elm · Exceptional Mirrors written in Elm."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 44,
"byteStart": 0
},
"features": [
{
"uri": "https://www.stackbuilders.com/news/reverse-reverse-theorem-proving-with-idris",
"$type": "pub.leaflet.richtext.facet#link"
}
]
}
],
"plaintext": "Reverse, Reverse: Theorem Proving with Idris"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": ": A blog post on how theorem proving works in Elm, detailing the classical vector reversal function's derivation."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 18,
"byteStart": 0
},
"features": [
{
"uri": "https://www.cs.ox.ac.uk/projects/utgp/school/idris-tutorial.pdf",
"$type": "pub.leaflet.richtext.facet#link"
}
]
}
],
"plaintext": "idris-tutorial.pdf"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": ": A short tutorial on Idris by Edwin Brady. Not sure how relevant it is to the newest versions of the language, but provides a compact overview of Idris' features."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 13,
"byteStart": 0
},
"features": [
{
"uri": "http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf",
"$type": "pub.leaflet.richtext.facet#link"
}
]
}
],
"plaintext": "Agda Tutorial"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 35,
"byteStart": 31
},
"features": [
{
"uri": "http://wiki.portal.chalmers.se/agda/pmwiki.php",
"$type": "pub.leaflet.richtext.facet#link"
}
]
}
],
"plaintext": ": Working on Idris led me to Agda which is a predecessor of Idris with an emphasis on theorem proving."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 42,
"byteStart": 0
},
"features": [
{
"uri": "http://stackoverflow.com/questions/42974540/how-can-i-express-range-validity-in-idris",
"$type": "pub.leaflet.richtext.facet#link"
}
]
}
],
"plaintext": "How can I express range validity in Idris?"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 205,
"byteStart": 171
},
"features": [
{
"$type": "pub.leaflet.richtext.facet#italic"
}
]
}
],
"plaintext": ": As I was struggling on writing some Idris code for my talk, I posted this question on SO which leads to a Ah!Ah! moment thanks to the answer it received: The slogan is Add more information to your types!"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 38,
"byteStart": 0
},
"features": [
{
"uri": "https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf",
"$type": "pub.leaflet.richtext.facet#link"
}
]
}
],
"plaintext": "Type Theory and Functional Programming"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": ": An out-of-print book by Simon Thompson (author of one of the first Haskell books) that seems to provide a lot of insights on top of Pierce's classical textbook."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 52,
"byteStart": 0
},
"features": [
{
"uri": "http://oxij.org/note/BrutalDepTypes/",
"$type": "pub.leaflet.richtext.facet#link"
}
]
}
],
"plaintext": "Brutal {Meta}Introduction to Dependent Types in Agda"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 87,
"byteStart": 78
},
"features": [
{
"uri": "http://augustss.blogspot.fr/2007/10/simpler-easier-in-recent-paper-simply.html",
"$type": "pub.leaflet.richtext.facet#link"
}
]
}
],
"plaintext": ": A page full of resources on dependent types, not only in Agda. Lead me to this post from Lennart Augustsson which gives an implementation of a depedently-typed lambda calculus in Haskell."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"index": {
"byteEnd": 12,
"byteStart": 0
},
"features": [
{
"uri": "https://medium.com/wardleymaps/finding-a-path-cdb1249078c0#.32oohi27s",
"$type": "pub.leaflet.richtext.facet#link"
}
]
}
],
"plaintext": "Wardley Maps"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [],
"plaintext": ": I have started again to read Simon Wardley's book-in-progress on how to draw maps for strategic thinking."
}
}
]
}
]
},
"publishedAt": "2017-03-28T00:00:00Z"
}