Skip to content

Instantly share code, notes, and snippets.

-- The following lets you write:
-- ghci> both @All Proxy (Proxy :: Proxy (TyApp Maybe)) Just (1, 'a')
-- (Just 1,Just 'a')
--
-- The type involved in that example is:
-- ghci> :t both @All Proxy (Proxy :: Proxy (TyApp Maybe))
-- both @All Proxy (Proxy :: Proxy (TyApp Maybe))
-- :: (forall r x. (All x, TyApp Maybe x r) => x -> r)
-- -> (a, b) -> (Maybe a, Maybe b)
@roboguy13
roboguy13 / groups.v
Created November 1, 2016 20:59
Groups in Coq
Definition assoc_law {g : Type} (op : g -> g -> g) :=
forall (x y z : g),
op (op x y) z = op x (op y z).
Definition left_iden_law {g : Type} (iden : g) (op : g -> g -> g) :=
forall (x : g),
op iden x = x.
Definition right_iden_law {g : Type} (iden : g) (op : g -> g -> g) :=
forall (x : g),
import Data.Word
import Control.Applicative
import Data.Vector (Vector)
type EmuWord = Word32
data Emu a -- ...
instance Functor Emu
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
import Control.Transformation
import Data.Functor.Yoneda
import Data.Functor.Coyoneda
instance Transformation ((->) a) g (Yoneda g a) where
Yoneda y # a = y a
@roboguy13
roboguy13 / Fac.hs
Last active August 29, 2015 14:26
examples/factorial let/app issues in HERMIT
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE CPP #-}
module Main where
import Prelude hiding ((*),(-))
import GHC.Exts
------------------------------------
@roboguy13
roboguy13 / .vimrc
Last active August 29, 2015 14:26
My current .vimrc
execute pathogen#infect()
augroup HighlightTODO
autocmd!
autocmd WinEnter,VimEnter * :silent! call matchadd('Todo', '\(TODO\)\|\(FIXME\)\|\(XXX\)\|\(NOTE\)', -1)
augroup END
" No beeps
set noerrorbells
set visualbell
@roboguy13
roboguy13 / DPair.hs
Last active August 29, 2015 14:25
Dependent pair types in Haskell
{-# LANGUAGE GADTs, ExistentialQuantification #-}
{-# LANGUAGE DataKinds, KindSignatures, TypeOperators #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ConstraintKinds #-}
-- Inspired by the dependent-sum package
import Data.Proxy
@roboguy13
roboguy13 / Client.hs
Created July 23, 2015 20:21
Deep embedding simulating simple Arduino
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
module Client where
import Prelude hiding (read)
import qualified Prelude
import Data.List
import Control.Monad
import Server
@roboguy13
roboguy13 / gist:2cba2baebdfaba033cbe
Created April 14, 2015 22:51
hask errors on GHC 7.10.1
$ cabal install hask
Warning: cannot determine version of /usr/local/bin/jhc :
""
Resolving dependencies...
Configuring hask-0...
Building hask-0...
Preprocessing library hask-0...
[1 of 9] Compiling Hask.Category ( src/Hask/Category.hs, dist/build/Hask/Category.o )
[2 of 9] Compiling Hask.Iso ( src/Hask/Iso.hs, dist/build/Hask/Iso.o )
[3 of 9] Compiling Hask.Functor.Faithful ( src/Hask/Functor/Faithful.hs, dist/build/Hask/Functor/Faithful.o )
% dist/build/accelerate-nofib/accelerate-nofib
accelerate-nofib (c) [2013] The Accelerate Team
Usage: accelerate-nofib [OPTIONS]
Available backends:
interpreter reference implementation (sequential)
* cuda implementation for NVIDIA GPUs (parallel)
prelude: