Skip to content

Instantly share code, notes, and snippets.

View silky's full-sized avatar

Noon van der Silk silky

563 followers · 7.8k following
View GitHub Profile
@silky
silky / typing.md
Created September 22, 2022 15:24 — forked from chrisdone/typing.md
Typing Haskell in Haskell

Typing Haskell in Haskell

MARK P. JONES

Pacific Software Research Center

Department of Computer Science and Engineering

Oregon Graduate Institute of Science and Technology

@silky
silky / default.nix
Created January 8, 2022 19:05 — forked from Gabriella439/default.nix
Nix build of vscode with haskell-language-server
let
nixpkgs = builtins.fetchTarball {
url = "https://github.com/NixOS/nixpkgs/archive/c473cc8714710179df205b153f4e9fa007107ff9.tar.gz";
sha256 = "0q7rnlp1djxc9ikj89c0ifzihl4wfvri3q1bvi75d2wrz844b4lq";
};
config = {
allowUnfree = true;
};
@silky
silky / CalcComp.hs
Created August 25, 2021 12:24 — forked from sjoerdvisscher/CalcComp.hs
Calculating Dependently-Typed Compilers
-- https://icfp21.sigplan.org/details/icfp-2021-papers/21/Calculating-Dependently-Typed-Compilers-Functional-Pearl-
{-# LANGUAGE GADTs, DataKinds, TypeOperators, TypeFamilies, TypeApplications, KindSignatures, ScopedTypeVariables #-}
import Control.Applicative
import Data.Kind
import Data.Type.Equality
type family (a :: Bool) || (b :: Bool) :: Bool where
'False || b = b
'True || b = 'True
@silky
silky / README.md
Created June 10, 2021 07:38 — forked from vivshaw/README.md
🙈🙉🙊 Three Wise Monkeys 🙈🙉🙊
@silky
silky / SizedNBE.hs
Created April 13, 2021 11:55 — forked from ekmett/SizedNBE.hs
Sized NBE using the same schema as the typed one, but with natural number sizes on environments
{-# Language CPP #-}
{-# Language BlockArguments #-}
{-# Language GADTs #-}
{-# Language RankNTypes #-}
{-# Language ViewPatterns #-}
{-# Language TypeApplications #-}
{-# Language BangPatterns #-}
{-# Language TypeOperators #-}
{-# Language TypeFamilyDependencies #-}
{-# Language DataKinds #-}
@silky
silky / Rec.hs
Created April 12, 2021 06:02 — forked from sjoerdvisscher/Rec.hs
{-# LANGUAGE DerivingStrategies, DerivingVia, TypeOperators, DataKinds,
DeriveGeneric #-}
module Rec where
import SameRepAs
import GHC.Generics ( Generic )
import qualified Data.Monoid as M
@silky
silky / maps.lean
Created February 10, 2021 12:15 — forked from brendanzab/maps.lean
Total and partial maps in Lean 4 (inspired by Software Foundations)
/-
Total and partial maps
This is inspired by [the relevant chapter in Software Foundations]. Unlike
Software Foundations, these maps are also parameterised over a `Key`
type, which must supply an implementation of `DecidableEq`.
[Software Foundations]: https://softwarefoundations.cis.upenn.edu/lf-current/Maps.html
-/
namespace Maps
@silky
silky / Trolling.hs
Created August 24, 2020 05:55 — forked from i-am-tom/Trolling.hs
Ramda-style composition where the first function must receive all arguments.
{-# LAnguage FlexibleInstances #-}
{-# LANGuage FunctionalDependencies #-}
{-# LANGUAge GADTs #-}
{-# LANGUAGE UndecidableInstances #-}
module Trolling where
---------------------------------------------------------------------
-- VARIADIC COMPOSITION IN HASKELL (A LA RAMDA.JS).
--
-- In Haskell, we typeically think of the composition operator (or
@silky
silky / dashboard.py
Created April 28, 2020 21:33 — forked from healeycodes/dashboard.py
# a simple dashboard for the waveshare 2in7b screen
# to be ran inside: https://github.com/waveshare/e-Paper/tree/master/RaspberryPi%26JetsonNano/python/examples
# 1. install the latest versions of `pyowm` and `requests`
# 2. edit `OPEN_WEATHER_KEY`, `LOCATION`, and `NEWS_API_KEY`
import sys
import os
picdir = os.path.join(os.path.dirname(os.path.dirname(os.path.realpath(__file__))), 'pic')
libdir = os.path.join(os.path.dirname(os.path.dirname(os.path.realpath(__file__))), 'lib')
if os.path.exists(libdir):
@silky
silky / linear_diophantine.py
Created January 21, 2020 21:44 — forked from pjt33/linear_diophantine.py
Count solutions to linear Diophantine equations
from collections import Counter
from fractions import Fraction
def _gcd(a, b):
while a:
a, b = b % a, a
return b