prozacchiwawa’s gists

prozacchiwawa / monadsample.hs

Created June 16, 2019 07:23

	import Text.Read

	-- Each invocation consumes strings from a stream
	-- So canonically, we apply ([String],()) yielding
	-- ([String],a)
	data SampleMonadValue a
	= SMV ([String] -> Either ([String],[String]) ([String],[String],a))

	sampleWrite :: String -> SampleMonadValue ()
	sampleWrite s = SMV $ \strings ->

prozacchiwawa / build.sh

Created February 23, 2019 21:33

AWS Lambda hacky bucklescript demo

	#!/bin/sh

	bsb -make-world
	browserify -o demo.js ./src/demo.bs.js
	(echo 'foo = exports \|\| {};' && cat demo.js) > demolambda.js

prozacchiwawa / ProofOfBin2NatIsReflexiveWithNat2Bin.idr

Last active July 18, 2018 13:48

ProofOfBin2NatIsReflexiveWithNat2Bin.idr

	{--

	Learning proof in idris.

	My first complete proof.

	Bin is a data type that uniquely represents Nat numbers in binary. It contains a representation
	only for a BNil element and "N zeros followed by a 1", which means that each Nat corresponds to
	precisely one Bin.

prozacchiwawa / Test.idr

Last active July 14, 2018 22:57

	{-- THIS IS AN EXAMPLE OF UNSOUND PROOF -- IT IS THE PRODUCT OF A CONFUSED MIND --}

	data Bin = O Nat Bin \| BNil

	{-
	total aNEBMeansNotEqual : (a : Nat) -> (b : Nat) -> (v : Bin) -> Dec (a = b) -> Dec (O a v = O b v)
	aNEBMeansNotEqual a b v (Yes prf) = rewrite prf in Yes Refl
	aNEBMeansNotEqual a b v (No contra) = No ?contraHell
	-}

prozacchiwawa / Minimal.idr

Last active June 19, 2018 23:01

	data IsEven : (b : Bool) -> Type where
	ItIsEven : IsEven True

	Uninhabited (IsEven False) where
	uninhabited IsEven impossible

	itHasTheOneBitSet : (n : Nat) -> Bool
	itHasTheOneBitSet Z = False
	itHasTheOneBitSet (S Z) = True
	itHasTheOneBitSet (S (S a)) = itHasTheOneBitSet a

prozacchiwawa / google-sheets-example.js

Created February 19, 2018 16:55

	var fs = require('fs');
	var readline = require('readline');
	var google = require('googleapis');
	var googleAuth = require('google-auth-library');

	// If modifying these scopes, delete your previously saved credentials
	// at ~/.credentials/sheets.googleapis.com-nodejs-quickstart.json
	var SCOPES = ['https://www.googleapis.com/auth/spreadsheets.readonly'];
	var TOKEN_DIR = (process.env.HOME \|\| process.env.HOMEPATH \|\|
	process.env.USERPROFILE) + '/.credentials/';

prozacchiwawa / test.fsx

Last active May 17, 2017 22:45

React attribute is incorrectly unwrapped

	#r "../node_modules/fable-core/Fable.Core.dll"
	#r "../node_modules/fable-powerpack/Fable.PowerPack.dll"
	#r "../node_modules/fable-react/Fable.React.dll"
	#r "../node_modules/fable-elmish/Fable.Elmish.dll"
	#r "../node_modules/fable-elmish-react/Fable.Elmish.React.dll"

	open Elmish
	open Elmish.React

	module R = Fable.Helpers.React

prozacchiwawa / Example.elm

Created April 13, 2017 14:00 — forked from kspeakman/Example.elm

JWT expiration notification

	-- Try to setup auto logout. But JWT parsing can fail in several ways.
	--
	-- Failure strategy:
	-- 1. Console log failure.
	-- 2. The fallback (not shown below) is to instruct the user to
	-- manually log out and back in when we receive 401 Unauthorized.
	--
	-- TODO send failure to logging infrastructure.

	notifyOnExpired : String -> Cmd Msg

prozacchiwawa / HmacSha256.elm

Created March 30, 2017 15:02

	module HmacSha256 exposing (hmac, packedStringOfIntArray, intArrayOfPackedString, presentableIntArray, presentationToIntArray)

	import Array exposing (Array)
	import Bitwise
	import Char
	import Debug exposing (log)
	import ParseInt as I
	{-- Note: relies on a modified version of billstclair's sha256 module with utf-8 handling disabled --}
	import Sha256 exposing (sha256)

prozacchiwawa / 𝙵𝚞𝚗𝚆𝚒𝚝𝚑.𝚎𝚕𝚖

Created February 4, 2017 07:19

arty prozacchiwawa