Skip to content

Instantly share code, notes, and snippets.

View MonoidMusician's full-sized avatar

Verity Scheel MonoidMusician

120 followers · 55 following
View GitHub Profile
@MonoidMusician
MonoidMusician / Comprehensive Errors.md
Last active February 18, 2022 21:46
Comprehensive Errors
@MonoidMusician
MonoidMusician / Main.purs
Created October 31, 2021 04:59
Validation example
module Main where
import Prelude
import Effect (Effect)
import Effect.Class (class MonadEffect)
import Halogen as H
import Halogen.Aff (awaitBody, runHalogenAff)
import Halogen.HTML as HH
import Halogen.HTML.Properties as HP
@MonoidMusician
MonoidMusician / CoercibleFunctor.hs
Last active September 16, 2021 00:43
{-# LANGUAGE QuantifiedConstraints, MultiParamTypeClasses #-}
module CoercibleFunctor where
import Prelude ()
import Data.Coerce (Coercible, coerce)
class (forall x y. Coercible x y => Coercible (f x) (f y)) => Functor f where
map :: forall a b. (a -> b) -> f a -> f b
@MonoidMusician
MonoidMusician / 0 metalanguage-grammar.bnf
Last active December 20, 2021 07:20
Sketches for Dhall-standard-as-data in Python using a type system à la PureScript
# Syntax for a metalanguage for writing programming language standards/specifications with an eye towards codegen
# The data format is very simple: data is either a string or a tuple of data.
# The idea is that we'll impose some simple types on top of this:
# Obviously strings, and arrays, possibly associative lists, and then mixed ADTs/enums, which are either plain strings or arrays where the first item is the tag denoting the constructor.
# I don't have the types figured out yet.
# Variable names
variable-name = [_A-Za-z][-_A-Za-z0-9]*
# A variable can have periods, but they don't mean anything
@MonoidMusician
MonoidMusician / Main.purs
Last active July 17, 2021 21:14
unsafe innerHTML in Halogen
module Main where
import Prelude
import Effect (Effect)
import Effect.Aff (Aff)
import Data.Maybe (Maybe(..))
import Halogen as H
import Halogen.Aff as HA
import Halogen.HTML as HH
@MonoidMusician
MonoidMusician / Main.purs
Last active July 17, 2021 20:46
innerHTML in Halogen
module Main where
import Prelude
import Effect (Effect)
import Effect.Aff (Aff)
import Data.Maybe (Maybe(..))
import Halogen as H
import Halogen.Aff as HA
import Halogen.HTML as HH
@MonoidMusician
MonoidMusician / cardinals_and_computability_theory.md
Last active February 21, 2021 18:15
Conversation on cardinals, computability, et cetera

Nick Scheel
what's the weakest type theory we can define arbitrary finite aleph numbers in? (arbitrary finite beth numbers are easy – just need natural numbers and functions)

Reed Mullanix
Be warned, the cardinals are not very well behaved in constructive math
Pretty much every direction you look, weird stuff starts to happen

Nick Scheel
yeah 🙂
I just find it weird that, with choice, all cardinals are aleph numbers, but beth numbers are the ones that are easy to construct in type theory

@MonoidMusician
MonoidMusician / Type Theory Notes.md
Last active January 3, 2023 21:16
Type Theory Notes

My research ideas

Implement a better typechecker for Dhall. Hopefully still straightforward to implement and with good errors.

I think it will essentially be a reification of the typechecker into data structures such that data still only flows one way, but acts like it flows both ways via substitution. Very tricky.

If I get it implemented, then I can look at performance.

Threads

@MonoidMusician
MonoidMusician / TestKindMatch.purs
Created January 29, 2021 18:49
module TestKindMatch where
import Prelude
import Data.Maybe (Maybe)
class Functor1 :: ((Type -> Type) -> Type) -> Constraint
class Functor1 t where
map1 :: forall f g. (f ~> g) -> t f -> t g
data Proxy :: forall k. k -> Type
@MonoidMusician
MonoidMusician / index.html
Created December 23, 2020 17:33
Simple web app to control mac volume & brightness
<html>
<head>
<meta charset="utf-8"/>
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<title>Control my mac</title>
<style>
/* From https://css-tricks.com/styling-cross-browser-compatible-range-inputs-css/ */
input[type=range] {
-webkit-appearance: none;
margin: 10px 0;