lambdageek

Keybase proof

I hereby claim:

• I am lambdageek on github.
• I am lambdageek (https://keybase.io/lambdageek) on keybase.
• I have a public key whose fingerprint is C867 1FA4 6A58 E491 4446 1ED4 E5FE 8828 BCB4 3EA2

To claim this, I am signing this object:

lambdageek

(* technically this is the lazy state monad.  In particular, note the return type of get *)
module type STATE_MONAD = 
  sig
    type ('a,'s) st

    val return : 'a -> ('a,'s) st
    val bind : ('a,'s) st -> ('a -> ('b, 's) st) -> ('b, 's) st
    val get : ('s Lazy.t, 's) st
    val modify : ('s -> 's) -> (unit, 's) st
    val put : 's -> (unit, 's) st

lambdageek

{-#
  LANGUAGE
    DeriveGeneric, DeriveDataTypeable,
    MultiParamTypeClasses,
    ViewPatterns
  #-}
-- A short example of an ML-style module system atop a core lambda calculus.
--
-- The core expression language has variables, applications and
-- lambdas and constants.  The type language has variables (of the single kind *)

lambdageek

Consider the following (not particularly useful) Haskell function

  f :: forall a . Eq a => a -> a -> ()
  f x y = if x == y then f [x, x] [y, y] else ()

My understanding is that this would be translated to something like

lambdageek

{-# LANGUAGE DataKinds, KindSignatures, GADTs, StandaloneDeriving, TypeFamilies #-}
module Bidirectional where

import Control.Applicative
import Control.Monad (when)

----------------------------------------
-- 'Flow d a' is like 'Maybe a' except the type index 'd' says whether
-- we're given a value or whether we want one.

lambdageek

-- |
-- Module     : Unbound.Generics.LocallyNameless.Alpha
-- Copyright  : (c) 2014, Aleksey Kliger
-- License    : BSD3 (See LICENSE)
-- Maintainer : Aleksey Kliger
-- Stability  : experimental
--
-- Use the 'Alpha' typeclass to mark types that may contain 'Name's.
{-# LANGUAGE DefaultSignatures
             , FlexibleContexts

lambdageek

Sometimes I want to put an array inside of a mathpartir inferrule.

The straightforward thing doesn't work:

\begin{equation*}
\inferrule{Conclusion}{
  Premiss 1 \and
  \begin{array}{ll}
 1 & 2 \\ % note, this is where the problem happens

lambdageek

{-# LANGUAGE PolyKinds, TypeOperators, TypeFamilies, KindSignatures, DataKinds, GADTs #-}
{-# OPTIONS_GHC -Wall #-}
module CommaSep where

-- classify tokens as either the empty token, or not 
data P = Empty | NonEmpty

-- space-separated token values 'a' with a kind index tracking whether they're populated
data Token a :: P -> * where
  -- the empty token

lambdageek

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PolyKinds, TypeOperators, TypeFamilies, KindSignatures, DataKinds, GADTs #-}
{-# OPTIONS_GHC -Wall #-}
-- | The C Pre-Processor, modeled.
--
-- I wanted to understand what happens in the C pre-processor when you put groups of tokens together.
-- It turns out that since C99, the pre-processor has "variadic macros" which essentially allow you to treat
-- comma-separated sequences of token ("parameter packs" in C spec terms) as some sort of grouping construct.
--
-- Initially, parameter packs seem pretty uninspiring... all you can do is capture a variable number of macro arguments and

lambdageek

using System;
using System.Reflection;
using System.Reflection.Emit;

class TestRefl {
	public static void Main (string[] args)
	{
		var ab = AssemblyBuilder.DefineDynamicAssembly (new AssemblyName ("Test"), AssemblyBuilderAccess.Run);
		var mb = ab.DefineDynamicModule ("Test");
		var tb = mb.DefineType ("TestG", TypeAttributes.Public);