silky

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 Haskell in Haskell

MARK P. JONES

Pacific Software Research Center

Department of Computer Science and Engineering

Oregon Graduate Institute of Science and Technology

silky

let
  nixpkgs = builtins.fetchTarball {
    url    = "https://github.com/NixOS/nixpkgs/archive/c473cc8714710179df205b153f4e9fa007107ff9.tar.gz";
    sha256 = "0q7rnlp1djxc9ikj89c0ifzihl4wfvri3q1bvi75d2wrz844b4lq";
  };

  config = {
    allowUnfree = true;
  };

silky

-- 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

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

silky

{-# Language CPP #-}
{-# Language BlockArguments #-}
{-# Language GADTs #-}
{-# Language RankNTypes #-}
{-# Language ViewPatterns #-}
{-# Language TypeApplications #-}
{-# Language BangPatterns #-}
{-# Language TypeOperators #-}
{-# Language TypeFamilyDependencies #-}
{-# Language DataKinds #-}

silky

{-# LANGUAGE DerivingStrategies, DerivingVia, TypeOperators, DataKinds,
             DeriveGeneric #-}

module Rec where

import SameRepAs
import GHC.Generics ( Generic )

import qualified Data.Monoid as M

silky

if you don't install the xinerama headers before compiling xmonad, then the x11 package doesn't build with xinerama support

solution: install the libxinerama-dev library before building xmonad

alternatively, if you didn't do that, then i just deleted the entire ~/.stack and .stack-work folders and rebuilt it. then it worked.

silky

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

{-# 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