Skip to content

Instantly share code, notes, and snippets.

View solomon-b's full-sized avatar

Solomon solomon-b

130 followers · 161 following
View GitHub Profile
@aradarbel10
aradarbel10 / Main.hs
Created December 6, 2022 15:40
A minimalistic example of bidirectional type checking for system F
{-# LANGUAGE StrictData, DerivingVia, OverloadedRecordDot #-}
{-
(compiled with GHC 9.4.2)
-}
{-
HEADS UP
this is an example implementation of a non-trivial type system using bidirectional type checking.
it is...
@vivshaw
vivshaw / README.md
Last active May 2, 2022 20:55
🙈🙉🙊 Three Wise Monkeys 🙈🙉🙊
@TOTBWF
TOTBWF / Categories.hs
Last active April 21, 2021 06:06
A Tenative Category Heirarchy
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoImplicitPrelude #-}
@alahijani
alahijani / Euclid.idr
Last active March 31, 2021 12:55
Proof of Euclid's Lemma in Idris - Number Theory Algorithms
module Euclid
import Syntax.PreorderReasoning
%default total
Divides : (divisor, dividend : Nat) -> Type
Divides d n = (q : Nat ** (n = q * d))
data Direction = LTR | RTL
@ChrisPenner
ChrisPenner / SemiRepresentable.hs
Created October 12, 2020 04:46
SemiRepresentable
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}
module SemiRepresentable where
import qualified Data.Map as M
import Numeric.Natural
import qualified Data.Set as S
import Data.These
@fiddlerwoaroof
fiddlerwoaroof / .gitignore
Last active September 21, 2021 19:28
Minimal Nix Docker
*.tar.gz
.sentinel.*
@i-am-tom
i-am-tom / FizzBuzz.hs
Last active June 26, 2023 16:35
Arguably the fastest implementation of FizzBuzz ever written.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UnsaturatedTypeFamilies #-}
import GHC.TypeLits
import Prelude hiding (Functor, Semigroup)
type Main = (Fizz <> Buzz) <$> (0 `To` 100)
@sevanspowell
sevanspowell / EmacsTooling.md
Last active July 6, 2022 01:11
A guide to setting up the Haskell tooling for Emacs in a Nix environment.

Running Emacs Haskell Tooling in a Nix environment

A guide to setting up the Haskell tooling for Emacs in a Nix environment.

Suggestions/Contact

mail@sevanspowell.net

Configuration

@LnL7
LnL7 / configure.sh
Last active June 9, 2020 20:13
darwin nix-daemon distributed builds
#!/usr/bin/env bash
sudo mkdir -p /run/nix/current-load
sudo launchctl unload /Library/LaunchDaemons/org.nixos.nix-daemon.plist
sudo rm /Library/LaunchDaemons/org.nixos.nix-daemon.plist
sudo curl -fsSL -o /Library/LaunchDaemons/org.nixos.nix-daemon.plist https://gist.github.com/LnL7/ba2eac19e77cd6b4bb02c8de03bf5f4e/raw/69722c2b13c4eb022a1312cd6891838b413e1f96/org.nixos.nix-daemon.plist
sudo launchctl load /Library/LaunchDaemons/org.nixos.nix-daemon.plist
# Configure /etc/nix/machines
# Make sure root can ssh to the builder (known_hosts etc.)
@Icelandjack
Icelandjack / OpenKinds.markdown
Last active January 26, 2020 20:53
Rethinking Tricky Classes: Explicit Witnesses of Monoid Actions, Semigroup / Monoid / Applicative homomorphisms