mafm

mafm

(* This is a demonstration of the use of the SML module system to
   encode (Generalized Algebraic Datatypes) GADTs via Church
   encodings. The basic idea is to use the Church encoding of GADTs in
   System Fomega and translate the System Fomega type into the module
   system. As I demonstrate below, this allows things like the
   singleton type of booleans, and the equality type, to be
   represented.

   This was inspired by Jon Sterling's blog post about encoding proofs
   in the SML module system:

mafm

from __future__ import unicode_literals
import sys

# We only use unicode in our parser, except for __repr__, which must return str.
if sys.version_info.major == 2:
    repr_str = lambda s: s.encode("utf-8")
    str = unicode
else:
    repr_str = lambda s: s

mafm

#!/usr/bin/env python2
#-*- coding: utf-8 -*-

# NOTE FOR WINDOWS USERS:
# You can download a "exefied" version of this game at:
# http://hi-im.laria.me/progs/tetris_py_exefied.zip
# If a DLL is missing or something like this, write an E-Mail ([email protected])
# or leave a comment on this gist.

# Very simple tetris implementation

mafm

(*
 * An OCaml implementation of final tagless, inspired from this article by Oleksandr Manzyuk:
 * https://oleksandrmanzyuk.wordpress.com/2014/06/18/from-object-algebras-to-finally-tagless-interpreters-2/
 *)

module FinalTagless = struct
  type eval = { eval : int }
  type view = { view : string }

  module type ExpT = sig

mafm

#!/usr/local/Gambit-C/bin/gsi

; Copyright (C) 2004 by Marc Feeley, All Rights Reserved.

; This is the "90 minute Scheme to C compiler" presented at the
; Montreal Scheme/Lisp User Group on October 20, 2004.

; Usage with Gambit-C 4.0:
;
;    % ./90-min-scc.scm test.scm

mafm

Require Import List.
Require Import FunctionalExtensionality.
Require Import ZArith.
Require Import Zcompare.

(* c.f. https://twitter.com/Hillelogram/status/987432184217731073 *)

Set Implicit Arguments.

Lemma map_combine : forall A B C (f : A -> B) (g : A -> C) xs,

mafm

import static java.lang.System.*;

import java.util.function.BiFunction;
import java.util.function.Function;

// Implementation of a pseudo-GADT in Java, translating the examples from
// http://www.cs.ox.ac.uk/ralf.hinze/publications/With.pdf
// The technique presented below is, in fact, just an encoding of a normal Algebraic Data Type
// using a variation of the visitor pattern + the application of the Yoneda lemma to make it
// isomorphic to the targeted 'GADT'.

mafm

--Roughly based on https://github.com/Gabriel439/Haskell-Morte-Library/blob/master/src/Morte/Core.hs by Gabriel Gonzalez et al.

data Expr = Star | Box | Var Int | Lam Int Expr Expr | Pi Int Expr Expr | App Expr Expr deriving (Show, Eq)

subst v e (Var v')       | v == v' = e
subst v e (Lam v' ta b ) | v == v' = Lam v' (subst v e ta)            b
subst v e (Lam v' ta b )           = Lam v' (subst v e ta) (subst v e b )
subst v e (Pi  v' ta tb) | v == v' = Pi  v' (subst v e ta)            tb
subst v e (Pi  v' ta tb)           = Pi  v' (subst v e ta) (subst v e tb)
subst v e (App f a     )           = App    (subst v e f ) (subst v e a )

mafm

type term =
  | Lam of (term -> term)
  | Pi of term * (term -> term)
  | Appl of term * term
  | Ann of term * term
  | FreeVar of int
  | Star
  | Box

let unfurl lvl f = f (FreeVar lvl)