Skip to content

Instantly share code, notes, and snippets.

@RyanGlScott
RyanGlScott / FromToVec.hs
Created Aug 28, 2021
Proofs involving conversion from and to length-indexed vectors
View FromToVec.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module FromToVec where
View ThePowerOfDefun.hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
-- Requires GHC 8.10 or later
module ThePowerOfDefun where
@RyanGlScott
RyanGlScott / Main.hs
Last active May 19, 2021
Is this use of unsafeCoerce valid?
View Main.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wall #-}
module Main (main) where
View GenericIso.hs
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeOperators #-}
module GenericIso where
import Data.Coerce
import GHC.Generics
@RyanGlScott
RyanGlScott / GADTSingletons.hs
Last active Oct 21, 2019
How to singletonize GADTs (requires GHC 8.2 or later)
View GADTSingletons.hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
@RyanGlScott
RyanGlScott / Retrofunctor.hs
Last active Sep 21, 2019
Profunctors, but in the other direction
View Retrofunctor.hs
module Retrofunctor where
import Control.Applicative
import Control.Arrow
import Data.Bifunctor.Biff
import Data.Bifunctor.Clown
import Data.Bifunctor.Flip
import Data.Bifunctor.Joker
import Data.Bifunctor.Product
import Data.Bifunctor.Sum
@RyanGlScott
RyanGlScott / TakesForeverToCompile.hs
Created Jul 21, 2019
Try compiling with -O1 if you have a lot of time on your hands
View TakesForeverToCompile.hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
@RyanGlScott
RyanGlScott / SingletonsVTA.hs
Created May 31, 2019
A sketch of how we might single visible type applications
View SingletonsVTA.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TopLevelKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
@RyanGlScott
RyanGlScott / QuickSort.v
Last active May 28, 2019
Correctness proof for QuickSort in Coq
View QuickSort.v
(* Largely inspired by https://github.com/coq/coq/wiki/QuickSort *)
Require Import Arith.Wf_nat Bool List Nat Omega.
Require Import Sorting.Permutation Sorting.Sorted.
Definition flip_ltb (x : nat) : nat -> bool :=
fun (y : nat) => y <? x.
Definition flip_geb (x : nat) : nat -> bool :=
fun (y : nat) => x <=? y.
@RyanGlScott
RyanGlScott / CTuples.hs
Last active May 16, 2019
Partially applicable constraint tuple type constructors
View CTuples.hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
#if __GLASGOW_HASKELL__ >= 708 && __GLASGOW_HASKELL__ < 710
{-# LANGUAGE NullaryTypeClasses #-}
#endif
#if __GLASGOW_HASKELL__ >= 800
{-# LANGUAGE UndecidableSuperClasses #-}