Skip to content

Instantly share code, notes, and snippets.

View jfdm's full-sized avatar

Jan de Muijnck-Hughes jfdm

  • University of Strathclyde
  • Europe
View GitHub Profile
@jfdm
jfdm / AocDay1.idr
Created December 5, 2023 14:50
I am not bored at work, I am exploring dependently-typed programming in practical settings.......
module AocDay1
import Decidable.Equality
import Data.List.Quantifiers
import Data.Singleton
import Data.String
data Length : Any p xs -> Nat -> Type where
Here : Length (Here p) Z
There : Length ltr n
@jfdm
jfdm / GeneratePlot.hs
Created November 23, 2023 17:54
Generating whisker plots from Hyperfine output.
#!/usr/bin/env cabal
{- cabal:
build-depends: base
, yaml
, text
, bytestring
-}
{-# LANGUAGE DeriveGeneric, OverloadedStrings, DuplicateRecordFields, DeriveAnyClass #-}
module Main where
@jfdm
jfdm / Flag.idr
Created October 2, 2023 10:48
Merge Sort in Idris...or 'a' solution to the dutch flag problem.
module Flag
import Control.Relation
import Control.WellFounded
import Data.Nat
import Data.DPair
import Data.List
import Data.List.Views
%default total
@jfdm
jfdm / MergeForSynthesis.org
Created August 24, 2023 14:29
Merging Local Types for Synthesis

Merging Local Types for Synthesis

This document is a literate Idris2 file that the compiler can understand, and if one uses polymode for eMacs can highlight…

In this document, we outline a proof of Merge For Synthesis for a simple representation of Local type. Merging this into Capable is going to be trifficult!

Preamble

module SystemF
import Decidable.Equality
import Data.SnocList.Elem
namespace Kind
public export
data Kind : Type
where ||| Types of Types
@jfdm
jfdm / Bar.idr
Last active March 28, 2023 13:14
Sample IPC between Idris and a process using Domain Sockets; an improvement would be to have `Client.idr` launch `Server.py` itself.
module Bar
import System
import System.File
import Data.String
namespace Main
export
main : IO ()
@jfdm
jfdm / urgh.tex
Created February 24, 2023 13:59
Variables in LaTeX using komascript.
\documentclass{article}
\usepackage{xspace}
% The Magic Sauce.
\usepackage{scrletter}
\makeatletter
\newkomavar[urghhh]{documentTitle}
\setkomavar{documentTitle}{\@title}
@jfdm
jfdm / annotated.html
Created December 6, 2022 17:04
A script to use katla to highlight modules in an idris project.
#!/bin/env bash
test ! -z $1 && set -x # Show commands if first arg is non-zero
mkdir -p build/html
katla_run()
{
KATLA_EXE=$(which katla)
test -x KATLA_EXE && echo "Katla not installed"
@jfdm
jfdm / main.ola
Last active October 16, 2022 19:35
Projection of Session Types in Ola (and we have a REPL)
role Alice
role Bob
type foo = String
protocol pingpong = Alice ==> Bob { ping(String)
. Bob ==> Alice { pong(String)
. end }}
main()
@jfdm
jfdm / Versioned.idr
Last active October 12, 2022 21:01
Indexing terms with versioning.
module Versioned
import Data.List.Elem
import Data.List.Quantifiers
import Data.Nat
%default total
data Ty
= TyNat