Skip to content

Instantly share code, notes, and snippets.

View cartazio's full-sized avatar

Carter Tazio Schonwald cartazio

319 followers · 27 following
View GitHub Profile
@thoughtpolice
thoughtpolice / algebras.hs
Last active December 10, 2015 08:58
Initial algebras and final coalgebras
{-# LANGUAGE RankNTypes, DeriveFunctor #-}
{-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}
module Main where
import Criterion.Main (defaultMain, bench, bgroup, nf)
--------------------------------------------------------------------------------
-- Fixed points of a functor
newtype Mu f = Mu { muF :: f (Mu f) }
@t0yv0
t0yv0 / subtyping.v
Last active February 28, 2021 01:47
Demonstrating TypeScript 0.8 type system to be unsound. The subtyping relationship is defined in a way that admits the following code that results in TypeError exception being thrown.
Require Import Utf8.
Inductive subtype (a b : Set) : Set :=
| ST : (a -> b) -> subtype a b.
Infix ":>" := subtype (at level 50).
Definition st {x y} f := ST x y f.
Definition unpack {a b : Set} (st : a :> b) :=
@dergachev
dergachev / GIF-Screencast-OSX.md
Last active May 2, 2024 05:55
OS X Screencast to animated GIF

OS X Screencast to animated GIF

This gist shows how to create a GIF screencast using only free OS X tools: QuickTime, ffmpeg, and gifsicle.

Screencapture GIF

Instructions

To capture the video (filesize: 19MB), using the free "QuickTime Player" application:

@copumpkin
copumpkin / Weird.agda
Last active March 14, 2023 09:32
Work in progress on seemingly impossible Agda, à la Escardó with a Luke Palmer flavor
module Weird where
open import Coinduction
open import Function
open import Data.Empty
open import Data.Product
open import Data.Conat
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Unary as U
@pchiusano
pchiusano / Process.hs
Created February 2, 2013 02:03
Stream transducer library
{-# Language ExistentialQuantification, GADTs #-}
module Control.Process where
import Data.Monoid
import Prelude hiding (zip, zipWith)
import Control.Applicative
import System.IO
data Process f a = Halt
@NicolasT
NicolasT / simd.hs
Last active December 13, 2015 20:58
Haskell SSE 128bit SIMD support in GHC 7.7.20130216 Compiled using ghc-7.7.20130216 -msse2 -O3 -fllvm -funbox-strict-fields -fforce-recomp -keep-llvm-files -optlo-O3 -optlc-O=3 -S simd.hs simd.ll and simd.s contain the 'most significant' parts of the compilation result.
{-# LANGUAGE MagicHash, UnboxedTuples, BangPatterns #-}
module Main where
import Data.Int
import System.Environment
import GHC.Int
import GHC.Prim
@sjoerdvisscher
sjoerdvisscher / LinearMap.hs
Last active December 17, 2015 03:59
Linear map category and products.
{-# LANGUAGE TypeFamilies, ConstraintKinds, GADTs, TypeOperators, UndecidableInstances #-}
{-# LANGUAGE CPP #-}
import Prelude hiding ((.))
import Data.VectorSpace
import Data.Category
import Data.Category.Limit
type a :* b = (a,b)
@NathanHowell
NathanHowell / curry.hs
Created May 31, 2013 23:36
A proof-of-concept demonstrating the use of Z3 to solve Cabal version constraints for Haskell packages
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE StandaloneDeriving #-}
@cartazio
cartazio / refs.md
Last active December 17, 2015 23:29
notes on the *.ll file grammar relevant reading :)
@reiddraper
reiddraper / test.hs
Created June 21, 2013 01:46
{-# LANGUAGE TemplateHaskell #-}
module Main
where
import System.Environment (getArgs)
import Data.ByteString.Char8 (pack)
import Control.Distributed.Process (say, Process, spawnLink, RemoteTable)
import Control.Distributed.Process.Node (newLocalNode, initRemoteTable, runProcess, localNodeId, LocalNode(..))
import Control.Distributed.Process.Internal.Types (NodeId(..))