Binary Lambda Calculus

The Binary Lambda Calculus (BLC) is a minimal, pure functional programming language invented by John Tromp in 2004 [1] based on a binary encoding of the untyped lambda calculus in De Bruijn index notation.

silky / typing.md

Created September 22, 2022 15:24 — forked from chrisdone/typing.md

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 / 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 / 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 / README.md

Created June 10, 2021 07:38 — forked from vivshaw/README.md

🙈🙉🙊 Three Wise Monkeys 🙈🙉🙊

If you want to see how it works, see the README on the repo.

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 / 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 / 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 / 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 / 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):

Noon van der Silk silky