mheiber

#lang typed/racket
; try this in Dr. Racket
(: bad-union  (All (k) (-> (U (Listof k) (Listof (Listof k))) (Listof k))))
(define (bad-union x) '())

(: use-bad-union Any)
(define (use-bad-union) (bad-union '()))

mheiber

// From "Refactoring" 2nd Edition by Martin Fowler

export default function createStatementData(invoice, plays) {
    const result = {};
    result.customer = invoice.customer;
    result.performances = invoice.performances.map(enrichPerformance);
    result.totalAmount = totalAmount(result);
    result.totalVolumeCredits = totalVolumeCredits(result);
    return result;

mheiber

trait A {}

struct SasA{}
impl A for SasA {}

trait Db<'d> {
    type Mem: ?Sized + A + 'd;
    fn d(&self) -> &Self::Mem;
}

mheiber

fn main() {
    let make_a = |n| move || n;
    let make_b = |n| move || n;
    vec![make_a(1), make_a(2)];
    vec![make_a(1), make_b(1)];
    vec![|| 1, || 1];
}

mheiber

Vim Advice

For best efficiency: Keep the Bindings, Leave the Editor

Most of the efficiency and joy of Vim is in the keybindings. All popular editors have Vim bindings. When first learning (and after), one can spare oneself a lot of pain by just focusing on the bindings.

The key idea is:

• "insert mode" is for inserting text, and that is all.
• "normal mode" is for navigating and manipulating code. Then all the keys can be used for useful things besides inserting text. What keys do is based mostly on easy-to-reachness and menmonics.

mheiber

" add visual indication of progress in a buffer to the status bar. To use:
" set statusline=%{ProgRock()}REST_OF_YOUR_STATUS_LINE HERE}
" for example:
" set statusline=%{ProgRock()}%{coc#status()}%{get(b:,'coc_current_function','')}
function! ProgRock()
    let magic_width_number = 30
    let width = winwidth(0)
    let lcur = line('.')
    let lend = line('$')
    let full = max([width - magic_width_number, 3])

mheiber

Theorem sum_equiv_visitor(A B C: Prop): A \/ B -> C <-> (A -> C) /\ (B -> C).
Proof.
  split.
  - auto.
  - destruct H; intro H0; destruct H0; auto.
Qed.

mheiber

Slogans about Mainstream Dependent Types

I find it can be hard for programmers to talk about dependent types, since we don't always have the same idea of what they are and they have a reputation of being hard to understand and implement. I want to share these slogans to (hopefully) make the conversation easier.

I wrote this in a hurry and would welcome comments with examples of "mainstream dependent types" - and any relevant corrections and links.

Note: "mainstream" is a moving target

1. "A dependent type is a type whose definition depends on a value."

mheiber

Ltac dubstep_goal F :=
  unfold F; fold F.

Ltac dubstep_in F H :=
  unfold F in H; fold F in H.

Tactic Notation "dubstep" constr(F)  := (dubstep_goal F).
Tactic Notation "dubstep" constr(F) "in" hyp(H) := (dubstep_in F H).

mheiber

set nocompatible
filetype off                  " required for Vundle
:set suffixesadd+=.js
nnoremap <leader><space> :noh<return>
nnoremap <leader><leader> :b#<CR>
nnoremap <leader>s :source ~/.vimrc<CR>
nnoremap <leader>q :xall<CR>
nnoremap <right> <C-w>10>
nnoremap <left> <C-w>10<
nnoremap <up> :resize -5<Cr>