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

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>

mheiber

-module(three).
-export([main/1]).

main(FileName) ->
    {ok, Device} = file:open(FileName, [read]),
    Cnt = device_counts(Device, maps:new()),
    io:format("~p", [Cnt]).

device_counts(Device, Map) ->
    case io:get_line(Device, "") of

mheiber

this content has moved! link coming soon

mheiber

Equality: Prior Art in Programming Languages

This document contains notes on how equality works in different programming languages, with a focus on immutable data types in functional languages.

OCaml

OCaml and Reason

OCaml has two equality primitives:

mheiber

PR comments on https://github.com/joeywatts/TypeScript/compare/joeywatts:private-named-instance-fields...joeywatts:private-named-instance-fields-transform-feedback?expand=1

It may be easier to have back and forth if this is converted into a temporary PR. That way we can do line comments.

• why error when private identifiers are used in JSX tag names? The following is allowed today, I don't see why private identifiers wouldn't be allowed as well.

class A {

mheiber

Should this error?

class Parent {
  #foo;
  copy(instance) {
    this.#foo = instance.foo;
  }
}
class Child extends Parent {}

mheiber

TypeScript's Type System as a Little Language

Theme: Thinking of type-level TS as a programming language

It has all the pieces!

• data:
  • objects, arrays, and tuples
• functions
• structured programming: