Skip to content

Instantly share code, notes, and snippets.

Avatar

Ryan Scott RyanGlScott

View GitHub Profile
@RyanGlScott
RyanGlScott / HDList.hs
Created Jul 23, 2022
Heterogeneous difference lists
View HDList.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module HDList where
import qualified Control.Category as Cat (Category(..))
import Data.Function (on)
@RyanGlScott
RyanGlScott / DList.v
Last active Jul 24, 2022
Proofs of the difference list invariant for various operations
View DList.v
Require Import Lists.List.
Import ListNotations.
Open Scope list_scope.
Require Import Logic.FunctionalExtensionality.
Require Import Lists.Streams.
Inductive DList (a : Type) : Type :=
| MkDList : (list a -> list a) -> DList a.
Arguments MkDList {a} f.
@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
@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
@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 #-}
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 / 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.
View gist:2404f1cee58152e1dd483d5b37a5ab7d
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NamedWildCards #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
module Foo where
import Data.Kind
View TypeLevelGlambda.hs
{-# 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