shhyou

AGDA_FILES=$(wildcard *.agda)
TEX_FILES=${AGDA_FILES:.agda=.tex}
PDF_FILES=${AGDA_FILES:.agda=.pdf}
MONO_FONT=DejaVu Sans Mono # FreeMono is another choice
PYGMENTS_STYLE=tango

GRADED_XOPP_FILES=$(wildcard *-graded.xopp)
GRADED_PDF_FILES=${GRADED_XOPP_FILES:.xopp=.pdf}

.PHONY: all

shhyou

#lang racket/gui
(require plot
         pict)

;;; Author: Laurent Orseau
;;; License: [Apache License, Version 2.0](http://www.apache.org/licenses/LICENSE-2.0) or
;;;          [MIT license](http://opensource.org/licenses/MIT) at your option.

;;; See in particular this blog bost:
;;; https://alex-hhh.github.io/2019/09/map-snip.html#2019-09-08-map-snip-footnote-2-return

shhyou

[
  {
      "key": "ctrl+shift+tab",
      "command": "workbench.action.previousEditor"
  },
  {
      "key": "ctrl+tab",
      "command": "workbench.action.nextEditor"
  }
]

shhyou

#|
building syntax objects
cpu time: 106 real time: 112 gc time: 45
expanding
cpu time: 16063 real time: 17360 gc time: 2152

building syntax objects 2
cpu time: 116 real time: 126 gc time: 50
expanding
cpu time: 15898 real time: 16583 gc time: 2231

shhyou

{- Coquand, T., & Dybjer, P. (1997). Intuitionistic model constructions and normalization proofs.
  Mathematical Structures in Computer Science, 7(1). https://doi.org/10.1017/S0960129596002150 -}

open import Data.Empty                            using (⊥)
open import Data.Unit                             using (⊤; tt)
open import Data.Nat                              using (ℕ; zero; suc)
open import Data.Product                          using (_×_; _,_; Σ; proj₁; proj₂; ∃-syntax)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong)

infix 3 _-→_ _-↛_

shhyou

Racket tips and tricks

These are extracted from discussions I triggered on the Racket Slack. Thanks to everyone who participated in the discussion threads! :-)

Conversion to boolean

Use (and value #t) to convert a value to its boolean equivalent.

Entering a module in the Racket REPL

shhyou

On hiring Haskellers

Recently I noticed the number of the same two questions being asked again and again on different Haskell resources. The questions were “How to get a Haskell job” and “Why is it so hard to find Haskellers?” Although these two are coming from the opposite sides of the hiring process, the answer is really just one. There is a single reason, a single core problem that causes difficulties of hiring and being hired in the Haskell community, and we should clearly articulate this problem if we want to increase the Haskell adoption.

We all know that there are many people wishing to get a Haskell job. And a visible increase of Haskell jobs looks like there should be a high demand for Haskellers. The Haskell community has also grown like crazy past years. But still, why is it so difficult to hire and to be hired? Why can’t companies just hire any single person who demonstrates a deep knowledge of Haskell in blog posts, in chats, on forums, and in talks? And why do Haskell companies avoid hirin

shhyou

With scoped effects, handlers must be a part of the program

It is seductive to imagine that effect handlers in an algebraic effect system are not part of the program itself but metalanguage-level folds over the program tree. And in traditional free-like formulations, this is in fact the case. The Eff monad represents the program tree, which has only two cases:

data Eff effs a where
  Pure :: a -> Eff effs a
  Op :: Op effs a -> (a -> Eff effs b) -> Eff effs b

data Op effs a where

shhyou

tmux cheatsheet

This cheatsheet is forked from henrik/tmux_cheatsheet.markdown.

As configured in my dotfiles.

Remember to start the shell with utf-8 supprt, by export LANG=utf-8 or similarly LC_ALL, LC_CTYPE.

start new:

shhyou

struct S { int i; };

S s;
S& func1() { return s; }
S func2() { return s; }

int main() {
  func1() = {5};
  func2() = {5};
  return 0;