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.)

The tooling and libraries change constantly and require migrations and reworkings due to upstream decision making (React). The language can't even handle equality (and this causes bugs) or ordering properly. We have all this infrastructure for generating types from Haskell, but they aren't the same in TypeScript (as it doesn't even have sum types), so you have to think in two different representations. We waste time on the poor quality type system. We have to do twice the work in terms of ferrying information to and from the server and think about data access patterns not just on the server but also on the client, versus a classic web app that just serves up HTML. The compiler is slow as hell, so it's not even faster than compiling Haskell code. The error messages for standard stuff are about as bad as using GHC with some exotic libraries. None of our Haskell expertise is useful (IOW wasted), things that are a one-liner in Haskell are 5 lines in TypeScript. Our app doesn't do anything fancy that a classic HTM

	-- 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.

	-- 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

	-- 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

	{-

	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

	(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))))

	FROM ubuntu:20.04

	RUN apt-get update -y
	RUN apt-get install -y python pip
	COPY . /home/chris/Work/alphacephei/vosk-server
	WORKDIR /home/chris/Work/alphacephei/vosk-server

	RUN pip install -r requirements.txt && pip3 install sounddevice
	RUN apt-get install -y libportaudio2


	chris@linux:~/Work/chrisdone-artificial/hell-1$ ghc -main-is main_native -O fib.hs -o fib && ./fib +RTS -s
	[1 of 2] Compiling Main ( fib.hs, fib.o ) [Flags changed]
	[2 of 2] Linking fib [Objects changed]
	832040
	50,864 bytes allocated in the heap
	3,272 bytes copied during GC
	44,328 bytes maximum residency (1 sample(s))
	25,304 bytes maximum slop
	6 MiB total memory in use (0 MiB lost due to fragmentation)

	-- named & hashmap; O(log n) update/access
	data Exp
	= Lam Int Expr
	\| Var Int
	\| App Exp Exp

	eval :: Map Int Expr -> Expr -> Expr
	eval env = \case
	App (Lam i b) e ->
	let !e' = eval e