Skip to content

Instantly share code, notes, and snippets.

Avatar
🐫
🐫.P(🐫) → ∅ ≡ (∃🐫.P(🐫)) → ∅

Yuriy Pitomets Pitometsu

🐫
🐫.P(🐫) → ∅ ≡ (∃🐫.P(🐫)) → ∅
View GitHub Profile
View HaskellBooks.md
  • Algorithm Design with Haskell
  • Beginning Haskell: A Project-Based Approach
  • Developing Web Apps with Haskell and Yesod
  • Functional Design and Architecture
  • Get Programming with Haskell
  • Haskell Book
  • Haskell Cookbook
  • Haskell Data Analysis Cookbook
  • Haskell Design Patterns
  • Haskell from the Very Beginning
@Pitometsu
Pitometsu / Term.java
Created May 19, 2020 — forked from jbgi/Term.java
Generalized Algebraic Data Types (GADT) in Java
View Term.java
import static java.lang.System.*;
import java.util.function.BiFunction;
import java.util.function.Function;
// Implementation of a pseudo-GADT in Java, translating the examples from
// http://www.cs.ox.ac.uk/ralf.hinze/publications/With.pdf
// The technique presented below is, in fact, just an encoding of a normal Algebraic Data Type
// using a variation of the visitor pattern + the application of the Yoneda lemma to make it
// isomorphic to the targeted 'GADT'.
@Pitometsu
Pitometsu / layout0.json
Last active May 6, 2020
Crysalis keyboard layout for keyboardio
View layout0.json
{
"keymap": [
{
"keyCode": 30,
"label": "1",
"extraLabel": "!"
},
{
"keyCode": 31,
"label": "2",
@Pitometsu
Pitometsu / layout0.json
Last active Mar 27, 2020
Chrysalis keyboardio layouts
View layout0.json
{
"keymap": [
{
"keyCode": 2079,
"label": "@"
},
{
"keyCode": 2078,
"label": "!"
},
@Pitometsu
Pitometsu / constraints.hs
Created Mar 13, 2020
constraints family
View constraints.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE PolyKinds #-}
import Data.Kind (Constraint)
type family All (c :: k -> Constraint) ts :: Constraint where All c '[] = (); All c (t:ts) = (c t, All c ts)
View hello_world.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE UnicodeSyntax #-}
@Pitometsu
Pitometsu / even.ml
Last active Dec 1, 2019
Even: Coq to OCaml
View even.ml
type _ num =
| Zero : zero num
| Succ : ('a num) -> 'a plus num
and _ plus = Plus : 'a num -> 'a plus
and zero = [ ]
;;
type _ even =
| Even_0 : zero num even
| Even_S : 'a num odd -> 'a plus num even
and _ odd =
@Pitometsu
Pitometsu / shell.nix
Created Nov 27, 2019
Coq environment
View shell.nix
let
overlays = [
(self: super: with self; {
coq = coq_8_10;
coq_8_10 = (super.coq_8_10.override { buildIde = false; });
coqPackages = coqPackages_8_10;
coqPackages_8_10 = (super.coqPackages_8_10.overrideScope' (self: super: {
inherit coq;
}));
})
View macos-ld-fix.nix
macos-ld-fix = stdenv.mkDerivation {
name = "macos-ld-fix";
src = null;
unpackPhase = "true";
dontBuild = true;
installPhase = ''
mkdir -p $out/opt/local/lib
'';
};
View functors.ml
module type M = sig
module type S
module S : S
end
;; module type M = sig module type S module S : S end