Skip to content

Instantly share code, notes, and snippets.

@cdepillabout
cdepillabout / magic1.hs
Created Apr 13, 2018
Example of running a function with a constraint of an instance that doesn't exist.
View magic1.hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
-- | This module shows how it is possible to run a function with a constraint of
-- an instance that doesn't exist.
--
-- For instance, in the 'f' function, the 'Lala' 'Int' instance doesn't exist,
@cdepillabout
cdepillabout / magic2.hs
Created Apr 13, 2018
Example of how it is possible to override the functions that get called for a typeclass.
View magic2.hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
-- | This modules shows how it is possible to override the functions that get
-- called for a typeclass.
--
-- For instance, the 'foo' function overrides the '(<>)' function for
@cdepillabout
cdepillabout / vect-with-sigma.hs
Created Apr 14, 2018
Show how to use Sigma from singletons with type-indexed lists.
View vect-with-sigma.hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
@cdepillabout
cdepillabout / existential-vs-sigma.hs
Last active Jun 11, 2021
This file shows how similar existential types are vs. sigma types (dependent pairs).
View existential-vs-sigma.hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
@cdepillabout
cdepillabout / exists.md
Last active Nov 7, 2018
encode "exists" from classic logic in Haskell using singletons
View exists.md

I was reading through Type Theory and Formal Proofs (recommended by @parsonsmatt), and there was some info about how to represent "exists" (Ǝ).

In the type-theory version of classical logic, "exists" can represented as a higher-order function using "forall" like the following:

Ǝ x : S. P x is defined as ∀ A : *. (∀ x : S. P x -> A) -> A
@cdepillabout
cdepillabout / my-ghc-8.6.2.nix
Created Nov 11, 2018
A length-indexed list where the length is ad-hoc polymorphic (using singletons)
View my-ghc-8.6.2.nix
let
nixpkgsTarball = builtins.fetchTarball {
name = "nixos-unstable-2018-11-09";
url = https://github.com/nixos/nixpkgs/archive/1c49226176d248129c795f4a654cfa9d434889ae.tar.gz;
sha256 = "0v8vp38lh6hqazfwxhngr5j96m4cmnk1006kh5shx0ifsphdip62";
};
nixpkgs = import nixpkgsTarball { };
in
@cdepillabout
cdepillabout / a-poset-lemma.hs
Created Nov 12, 2018
proving a lemma about least elements in posets in Haskell using singletons
View a-poset-lemma.hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
View list-of-flags.txt
'--cc=/nix/store/10yq7kwlvbc6h658izmrlsspry1g9f3c-gcc-wrapper-7.3.0/bin/cc'
'--cflag=-D__GLASGOW_HASKELL__=804'
'--cflag=-Dlinux_BUILD_OS=1'
'--cflag=-Dlinux_HOST_OS=1'
'--cflag=-Dx86_64_BUILD_ARCH=1'
'--cflag=-Dx86_64_HOST_ARCH=1'
'--cflag=-I.stack-work/dist/x86_64-linux-nix/Cabal-2.2.0.1/build/autogen'
'--cflag=-I.stack-work/dist/x86_64-linux-nix/Cabal-2.2.0.1/build/global-autogen'
'--cflag=-I/home/illabout/.stack/snapshots/x86_64-linux-nix/lts-12.13/8.4.3/lib/x86_64-linux-ghc-8.4.3/network-2.6.3.6-2g6VId0Xlc85XRtUcfQj0T/include'
'--cflag=-I/home/illabout/.stack/snapshots/x86_64-linux-nix/lts-12.13/8.4.3/lib/x86_64-linux-ghc-8.4.3/primitive-0.6.3.0-DaZpcxwJp2TGn8ITSgfI4C/include'
View envvar.txt
AR=ar
AR_FOR_TARGET=ar
AS=as
AS_FOR_TARGET=as
CC=gcc
CC_FOR_TARGET=gcc
CONFIG_SHELL=/nix/store/r47p5pzx52m3n34vdgqpk5rvqgm0m24m-bash-4.4-p23/bin/bash
CXX=g++
CXX_FOR_TARGET=g++
DISPLAY=localhost:10.0
View gist:5485f1160b8597eede7790a1722f5b5f
these derivations will be built:
/nix/store/x5bvnh074wh774yd3n73zgylicjxf408-gi-gdk-3.0.16.drv
/nix/store/8smaas6jq95knzqbw6inlfhlw97bla0y-gi-gtk-3.0.25.drv
/nix/store/4a8avkmjxv5sb30qzcshshlx92pwwww0-gi-vte-2.91.19.drv
/nix/store/912iwrga7jvxn3vawab29hmnfsrpsv3z-termonad-1.0.0.0.drv
/nix/store/br77czswyk786k0ak8j4hwradp2xxbxw-ghc-8.4.4-with-packages.drv
/nix/store/g8gags5q5hiiqpzxx45y1kwzf0xkvmf9-termonad-with-packages-8.4.4.drv
building '/nix/store/x5bvnh074wh774yd3n73zgylicjxf408-gi-gdk-3.0.16.drv'...
setupCompilerEnvironmentPhase
Build with /nix/store/dxljd69cp3m5cgfl53h0fjbq202m0fm7-ghc-8.4.4.