Skip to content

Instantly share code, notes, and snippets.

View w.v
Require Import List.
Import ListNotations.
Require Import Relations Arith.
Definition on {A B : Type} (RB : relation B) (f : A -> B) : relation A :=
fun a a' => RB (f a) (f a').
Lemma wf_apply : forall (A B : Type)
(RA : relation A) (RB : relation B) (f : A -> B),
(forall a a', RA a a' -> RB (f a) (f a')) ->
View gtrav.hs
{-# LANGUAGE DeriveAnyClass, DeriveGeneric, DataKinds, PolyKinds, GADTs, TypeOperators, RankNTypes, ScopedTypeVariables, TypeApplications #-}
import Generics.SOP
import qualified GHC.Generics as GHC (Generic)
import Data.Proxy
type Optic f s a = (a -> f a) -> (s -> f s)
type Trav s a = forall f. Applicative f => Optic f s a
newtype Trav_ s a = Trav_ (Trav s a)
View FlexibleId.hs
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DerivingStrategies #-}
View IndexSOP.hs
{-# LANGUAGE
ConstraintKinds,
DataKinds,
PolyKinds,
GADTs,
FlexibleInstances,
MultiParamTypeClasses,
ScopedTypeVariables,
TypeFamilies,
TypeApplications,
View pop.idr
module Main
data Stack_ : Type -> Type where
Empty : Stack_ a
One : Stack_ a -> Stack_ a
-- This is intentionally oversimplified to be the identity function
-- It's just what's left from erasing all irrelevant domain-specific details
-- so we can focus on Idris's type system.
View CompactStack.idr
{-
This is a proof about the amortized complexity of a
stack data structure which works by concatenating and
splitting arrays whose lengths are powers of two.
(Stack, push, pop).
(This is a formalization of https://github.com/treeowl/compact-sequences
where I already wrote this in Coq, but linear types would help make it more
precise.)
View pop.idr
module Main
import Data.Nat
data Stack_ : Type -> Type where
Empty : Stack_ a
One : Stack_ a -> Stack_ a
pop_ : Stack_ a -> Stack_ a
View error.idr
module Main
import Data.Nat
data Stack_ : Type -> Type where
Empty : Stack_ a
One : Stack_ a -> Stack_ a
pop_ : Stack_ a -> Stack_ a
pop_ Empty = Empty
View error.idris
module Main
import Data.Nat
-- Linearity
infixr 0 #->, ?->
(#->) : Type -> Type -> Type
a #-> b = (1 _ : a) -> b
View error.idris
module Main
import Data.Nat
data Stack_ : Nat -> Type -> Type where
Two : (1 _ : Stack_ (2 * i) a) -> Stack_ i a
data Debits_ : Nat -> Stack_ i a -> Type where
DTwo : (1 _ : Debits_ (i + acc) s) -> Debits_ acc (Two s)
You can’t perform that action at this time.