Chris Done chrisdone-artificial

This program can:

Take an untyped AST (UTerm) which is easy to parse, for a little language that has bools, strings, lambdas, if and pure/bind.
By type checking it, convert it into a well-typed GADT.
That well-typed GADT can then be trivially interpreted via eval which is total.
It's easy to add functions of N-arity by adding a PrimN constructor.

An example program which features using IO to check whether a file exists and then writing a file depending on that condition, is at the end.

The type-checker just throws an error via error or a pattern match failure, but that's trivial to turn into an Either. The eval, however, throws no errors. (Although I/O code produced by it may, obviously.)

You need to enable dom.events.asyncClipboard.clipboardItem for it to work, via about:config.

	(defmacro z (expr)
	(z-unintern 0 (z-rename (z-intern-expr expr))))

	(defun z-intern-expr (expr)
	(cond
	((and (consp expr)
	(eq 'lambda (car expr)))
	(list :tag '$lam
	:var (caadr expr)
	:body (z-intern-expr (caddr expr))))

	{-

	Examples:

	> reify @Int $ eval $ A (reflect (abs :: Int -> Int)) (I (-9))
	9

	> reify @Int $ eval $ A (A (reflect ((*) :: Int -> Int -> Int)) (reflect @Int 3)) (reflect @Int 5)
	15

	-- Written by Eitan Chatav, cleaned up by me

	{-# language GADTs #-}
	module Wibble where

	import Type.Reflection
	import Data.Constraint

	data U_Expr
	= U_Bool Bool

	-- Written by Eitan Chatav, cleaned up by me

	{-# language GADTs #-}

	import Type.Reflection
	import Data.Constraint

	data U_Expr
	= U_Bool Bool
	\| U_Int Int

	-- original from <https://www.cs.ox.ac.uk/projects/gip/school/tc.hs> but URLs don't last long in academia
	--
	{-# LANGUAGE ExistentialQuantification,GADTs #-}

	-- This typechecker, written by Stephanie Weirich at Dagstuhl (Sept 04)
	-- demonstrates that it's possible to write functions of type
	-- tc :: String -> Term a
	-- where Term a is our strongly-typed GADT.
	-- That is, generate a typed term from an untyped source; Lennart
	-- Augustsson set this as a challenge.

	{-# LANGUAGE GADTs #-}
	{-# LANGUAGE OverloadedRecordDot #-}
	{-# LANGUAGE UndecidableInstances #-}

	module Brossa.Authorization where

	-- brossa-specific

	import qualified Brossa.DB.Rel8 as BrossaRel8
	import qualified Brossa.DB.Hasql as BrossaHasql

	(define-derived-mode shoe-mode
	fundamental-mode "Shoe"
	"Auto-paging shell mode..
	\\{shoe-mode-map}"
	(linum-mode -1))

	(defconst shoe-dir "~/.shoe")

	(defvar shoe-shell-program "/bin/bash")