Skip to content

Instantly share code, notes, and snippets.

module Printf
%default total
data Format = FInt Format -- %d
| FString Format -- %s
| FOther Char Format -- [a-zA-Z0-9]
| FEnd --
format : List Char -> Format
@david-christiansen
david-christiansen / FizzBuzzC.idr
Last active August 29, 2022 20:00
Dependently typed FizzBuzz, now with 30% more constructive thinking
module FizzBuzzC
%default total
-- Dependently typed FizzBuzz, constructively
-- A number is fizzy if it is evenly divisible by 3
data Fizzy : Nat -> Type where
ZeroFizzy : Fizzy 0
Fizz : Fizzy n -> Fizzy (3 + n)
@puffnfresh
puffnfresh / reornament.idr
Last active September 15, 2018 21:20
Algebraic Ornaments!
module reornament
-- Idris translation of Agda code:
-- https://gist.github.com/gallais/e507832abc6c91ac7cb9
-- Which follows Conor McBride's Ornaments paper:
-- https://personal.cis.strath.ac.uk/conor.mcbride/pub/OAAO/Ornament.pdf
ListAlg : Type -> Type -> Type
ListAlg A B = (B, A -> B -> B)
@djspiewak
djspiewak / streams-tutorial.md
Created March 22, 2015 19:55
Introduction to scalaz-stream

Introduction to scalaz-stream

Every application ever written can be viewed as some sort of transformation on data. Data can come from different sources, such as a network or a file or user input or the Large Hadron Collider. It can come from many sources all at once to be merged and aggregated in interesting ways, and it can be produced into many different output sinks, such as a network or files or graphical user interfaces. You might produce your output all at once, as a big data dump at the end of the world (right before your program shuts down), or you might produce it more incrementally. Every application fits into this model.

The scalaz-stream project is an attempt to make it easy to construct, test and scale programs that fit within this model (which is to say, everything). It does this by providing an abstraction around a "stream" of data, which is really just this notion of some number of data being sequentially pulled out of some unspecified data source. On top of this abstraction, sca

@AndrasKovacs
AndrasKovacs / Inord.idr
Created June 7, 2015 10:31
The (positions of elements in a binary tree) and (the positions in its inorder traversal) are isomorphic.
import Data.List
%default total
data Tree : Type -> Type where
Tip : Tree a
Node : (x : a) -> (l : Tree a) -> (r : Tree a) -> Tree a
%name Tree t, u
data InTree : a -> Tree a -> Type where
@pbl64k
pbl64k / adt.idr
Created August 18, 2015 09:54
...need indexed functors...
%default total
data Id : Type -> Type where
I : a -> Id a
data Const : (a : Type) -> (b : Type) -> Type where
K : a -> Const a b
data Sum : (a : Type -> Type) -> (b : Type -> Type) -> (c : Type) -> Type where
SumL : a c -> Sum a b c
@raichoo
raichoo / coyo.idr
Last active October 26, 2017 22:27
Using Coyoneda to improve performance in Idris
module Main
{-
Strictness always bothers me a little, since it forces you to do
things like fusion manually. This prohibits code reuse. I won't
elaborate on this too much since there is already a great blog
post about this:
http://augustss.blogspot.co.uk/2011/05/more-points-for-lazy-evaluation-in.html
object Example {
implicit val es = Executors.newCachedThreadPool
val metrics = new MetricsCollectorImpl(MetricsCollectorConfiguration("example", "localhost", 8125))
val ironConfig: IronMqConfig = ???
val iron = IronMqMessaging(ironConfig, QueueName("example-queue"))
def main(args: Array[String]) {
val consumer = StreamMq(iron, metrics).consumer
@gkossakowski
gkossakowski / asSeenFrom.md
Last active June 19, 2018 18:27
Understand Scala's core typechecking rules

Scala's "type T in class C as seen from a prefix type S" with examples

Introduction

Recently, I found myself in need to precisely understand Scala's core typechecking rules. I was particulary interested in understanding rules responsible for typechecking signatures of members defined in classes (and all types derived from them). Scala Language Specification (SLS) contains definition of the rules but lacks any examples. The definition of the rules uses mutual recursion and nested switch-like constructs that make it hard to follow. I've written down examples together with explanation how specific set of rules (grouped thematically) is applied. These notes helped me gain confidence that I fully understand Scala's core typechecking algorithm.

As Seen From

Let's quote the Scala spec for As Seen From (ASF) rules numbered for an easier reference:

@gabriel-fallen
gabriel-fallen / SampleTheorems.idr
Last active June 28, 2017 09:46
A proof in Idris that `reverse . reverse = id`
module SampleTheorems
%default total
reverse' : List a -> List a
reverse' [] = []
reverse' (x :: xs) = reverse' xs ++ [x]
append_nil : xs ++ [] = xs
append_nil {xs = []} = Refl