liamoc

[{"contents":[0,"A Holbert PL Semantics Exercise"],"tag":"Heading"},{"contents":"This is a series of small exercises designed to help you get familiar with Holbert. So that you will not need to type cumbersome prefix notation, we define some syntax here.","tag":"Paragraph"},{"contents":[2,"_/\\_","LeftAssoc"],"tag":"SyntaxDecl"},{"contents":[1,"_\\/_","LeftAssoc"],"tag":"SyntaxDecl"},{"contents":[5,"not_","NonAssoc"],"tag":"SyntaxDecl"},{"contents":[0,"_BExp","NonAssoc"],"tag":"SyntaxDecl"},{"contents":[0,"_IExp","NonAssoc"],"tag":"SyntaxDecl"},{"contents":[1,"if_then_else_","LeftAssoc"],"tag":"SyntaxDecl"},{"contents":[0,"_Bool","NonAssoc"],"tag":"SyntaxDecl"},{"contents":[0,"_eval_","NonAssoc"],"tag":"SyntaxDecl"},{"contents":[0,"_eval","NonAssoc"],"tag":"SyntaxDecl"},{"contents":[0,"_|->_","NonAssoc"],"tag":"SyntaxDecl"},{"contents":[0,"_~=_","NonAssoc"],"tag":"SyntaxDecl"},{"contents":[0,"let_in_","NonAssoc"],"tag":"SyntaxDecl"},{"contents":[1,"The Language I of Boolean Decisions"],"tag":"Heading"},{"cont

liamoc

A few thoughts below about this anonymous person threatening two female academics in my area. Roopsha for complaining about discrimination at Perdue where she was denied tenure (for speaking up?) and Talia for vocally supporting her.

I think this person is awful and feel for both Roopsha and Talia for receiving such threats. Opinion aside, they are pointing to potential problems in the tenure system and potential harms that can come from complaining about sexism and discrimination.

This could be valuable information. From an information theoretic perspective, information identifying the reasons for systems not to operate as we want them is valuable in learning how to improve the systems. With that said, what are the shortages this person identified?

First, they are describing a potentially problematic structure communities that can cause major harm in speaking up. Namely, small communities with lots of friendships (conflicts of interest) and how in such structure criticising powerful entities could result

liamoc

section 
parameters {α : Type} 
variable [ a_dec  : decidable_eq α]
include a_dec
open nat 

definition replicate (a : α) : ℕ → list α 
| 0 := []
| (succ n) := a :: replicate n

liamoc

0. Install rosetta, command line tools, etc.
1. install gnu tar, gnu coreutils and bash from brew.
2. compile this dylib https://github.com/yairchu/macos11-haskell-workaround
3. clone ghcjs 8.6 branch and submodules
4. install ghc 8.6 and cabal-install 2.4 with ghcup
5. Edit the ghcup ghc wrapper script to add the dylib to DYLD_INSERT_LIBRARIES before invoking ghc
6. Edit the ./ghc/aclocal.m4 and remove the underscore before AC_
7. Edit the ./utils/makePackages.sh to use the brew-installed bash
8. Run the makePackages script
9. Run cabal install, have a cup of tea

liamoc

#include <stdio.h>

/* BEGIN HACKERY */

typedef struct field {
    enum {
      TABLE_NAME,
      TABLE_FIELD,
      TABLE_TERMINATOR
    } tag;

liamoc

module bugreport where

open import Data.Nat 
open import Data.Bool hiding (_≟_)
open import Relation.Nullary

⸤_⸥ : {A : Set} → Dec A → Bool
⸤ yes _ ⸥ = true 
⸤ no  _ ⸥ = false 

liamoc

{-# LANGUAGE GADTs, KindSignatures #-}
module FakeWebFramework (add , notActuallyAWebFramework, get, Handler', link) where

import UrlPath
import Control.Monad.Writer 
import Data.Maybe

maybeRead :: (Read a) => String -> Maybe a
maybeRead s = case reads s of
  [(x, "")] -> Just x

liamoc

// needs -fnested-functions. Can be done without, but makes the whole thing a lot more cumbersome
// and less useful.
#include <stdio.h>

#define my_data_alts  ( void (*A)(int) , void (*B)(int, int) , void (*C)(char, int) )
#define make_my_data(n) void n my_data_alts
typedef void (*my_data) my_data_alts;


void show(my_data match) {

liamoc

{-# LANGUAGE OverloadedStrings #-}
module Main where

import Data.Yaml
import System.Environment
import Control.Applicative

data Whatever = Foo { courses :: [String], required :: Int } deriving Show

instance FromJSON Whatever where

liamoc

{-# LANGUAGE GADTs, DataKinds, KindSignatures, FlexibleInstances, ScopedTypeVariables #-}

import Test.QuickCheck
import Test.QuickCheck.Gen
import Control.Applicative
import Data.List

-- Peano naturals (used on value and type level)
data Nat = Zero | Suc Nat