Skip to content

Instantly share code, notes, and snippets.

View RyanGlScott's full-sized avatar

Ryan Scott RyanGlScott

258 followers · 0 following
View GitHub Profile
@RyanGlScott
RyanGlScott / QuickSort.v
Last active August 19, 2024 11:07
Correctness proof for QuickSort in Coq
(* 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 / gist:2404f1cee58152e1dd483d5b37a5ab7d
Last active May 16, 2019 13:16
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NamedWildCards #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
module Foo where
import Data.Kind
@RyanGlScott
RyanGlScott / TypeLevelGlambda.hs
Last active February 23, 2019 13:19
Type-level glambda
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
-- | Requires GHC 8.8 or later
module TypeLevelGlambda where
@RyanGlScott
RyanGlScott / Bug.hs
Created February 13, 2019 16:36
Pattern synonym existential scoping weirdness
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Bug where
import Data.Kind
import Data.Proxy
data T = forall k (a :: k). MkT (Proxy a)
@RyanGlScott
RyanGlScott / gist:dba49db44881735c3476e8b2483e25d1
Last active May 16, 2019 13:19
{-# LANGUAGE RankNTypes #-}
module Bug where
import Data.Functor.Identity
newtype T f = MkT { unT :: forall a. f a }
works1 :: T Identity -> T Identity
works1 (MkT x) = MkT x
@RyanGlScott
RyanGlScott / Foo.hs
Last active January 9, 2019 14:01
Can you implement `foo` without `coerce`?
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module Foo where
import Data.Coerce
type family F a
newtype T1 = MkT1 (forall a. F a)
newtype T2 = MkT2 (forall a. F a)
@RyanGlScott
RyanGlScott / SubstRep1.hs
Last active December 11, 2018 13:49
How to derive a Generic instance using nothing but Generic1
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module SubstRep1 where
@RyanGlScott
RyanGlScott / CTuples.hs
Last active May 16, 2019 13:35
Partially applicable constraint tuple type constructors
{-# 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 #-}
@RyanGlScott
RyanGlScott / S.hs
Last active November 30, 2018 17:18
Conor McBride's S combinator in GHC
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module S where
import Data.Kind
@RyanGlScott
RyanGlScott / ElimNat.hs
Last active November 14, 2018 20:07
Type-level eliminators in GHC!
#!/usr/bin/env cabal
{- cabal:
build-depends: base >= 4.12
, singleton-nats >= 0.4.1
, singletons >= 2.5.1
-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}