MARK P. JONES
Pacific Software Research Center
Department of Computer Science and Engineering
Oregon Graduate Institute of Science and Technology
let | |
nixpkgs = builtins.fetchTarball { | |
url = "https://github.com/NixOS/nixpkgs/archive/c473cc8714710179df205b153f4e9fa007107ff9.tar.gz"; | |
sha256 = "0q7rnlp1djxc9ikj89c0ifzihl4wfvri3q1bvi75d2wrz844b4lq"; | |
}; | |
config = { | |
allowUnfree = true; | |
}; |
-- 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 |
If you want to see how it works, see the README on the repo.
{-# Language CPP #-} | |
{-# Language BlockArguments #-} | |
{-# Language GADTs #-} | |
{-# Language RankNTypes #-} | |
{-# Language ViewPatterns #-} | |
{-# Language TypeApplications #-} | |
{-# Language BangPatterns #-} | |
{-# Language TypeOperators #-} | |
{-# Language TypeFamilyDependencies #-} | |
{-# Language DataKinds #-} |
{-# LANGUAGE DerivingStrategies, DerivingVia, TypeOperators, DataKinds, | |
DeriveGeneric #-} | |
module Rec where | |
import SameRepAs | |
import GHC.Generics ( Generic ) | |
import qualified Data.Monoid as M |
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.
/- | |
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 |
{-# 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 |
# 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): |