Nada Amin namin

Principled Meta Programming for Scala

This note outlines a principled way to meta-programming in Scala. It tries to combine the best ideas from LMS and Scala macros in a minimalistic design.

LMS: Types matter. Inputs, outputs and transformations should all be statically typed.
Macros: Quotations are ultimately more easy to deal with than implicit-based type-lifting
LMS: Some of the most interesting and powerful applications of meta-programming

	;; Traditional Abstract DPLL (no clause learning)
	;; See this paper: https://homepage.cs.uiowa.edu/~tinelli/papers/NieOT-JACM-06.pdf
	#lang racket

	(define (clause? cl)
	(match cl
	[`(,(? integer? x) ...) #t]
	[_ #f]))

	import chess
	import chess.engine
	import os
	import dspy
	from pydantic import BaseModel, Field
	from dspy.functional import TypedPredictor
	from dotenv import load_dotenv


	load_dotenv()

	import torch

	import outlines.models as models

	from outlines.text.generate.regex import choice
	from outlines.text.generate.continuation import continuation
	from outlines.text.generate.sample import greedy


	def make_greedy_tracker(generator):

	<!DOCTYPE html>
	<html lang="en">
	<head>
	<meta charset="utf-8" />
	<meta name="viewport" content="width=device-width, initial-scale=1" />
	<title>scratch</title>
	<style>
	body {
	font-family: Hack, Menlo, Monaco, 'Droid Sans Mono', 'Courier New', monospace;
	white-space: pre;

	-- The meta-circular interpreter from section 5 of Reynolds's Definitional
	-- Interpreters for Higher Order Programming Languages
	-- (http://www.cs.uml.edu/~giam/91.531/Textbooks/definterp.pdf)

	data EXP
	= CONST Const
	\| VAR Var
	\| APPL Appl
	\| LAMBDA Lambda
	\| COND Cond

	object unsoundForwardRef {
	trait LowerBound[T] {
	type M >: T;
	}
	trait UpperBound[U] {
	type M <: U;
	}

	val bounded1 : LowerBound[Int] with UpperBound[String] = hideForwardRef

	-- Here I relate problem with unrealizable contexts in μDOT with known problems
	-- in dependent type theory. I use Agda for illustration.
	--
	-- I also discuss the viewpoint given by denotational semantics.

	module SoundnessOpenTermsXiRule where

	open import Relation.Binary.PropositionalEquality
	open import Data.Nat
	open import Data.Bool

	miles@frege:~$ scala
	Welcome to Scala version 2.11.0 (Java HotSpot(TM) 64-Bit Server VM, Java 1.7.0_55).
	Type in expressions to have them evaluated.
	Type :help for more information.

	scala> import scala.language.dynamics
	import scala.language.dynamics

	scala> case class Assoc[K, V](value: V)
	defined class Assoc

	scala> trait Assoc[K] { type V ; val value: V }
	defined trait Assoc

	scala> def mkAssoc[V0](k: String, v: V0): Assoc[k.type] { type V = V0 } =
	\| new Assoc[k.type] { type V = V0 ; val value = v }
	mkAssoc: [V0](k: String, v: V0)Assoc[k.type]{type V = V0}

	scala> implicit def nameAssoc = mkAssoc("Name", "Mary")
	nameAssoc: Assoc[String("Name")]{type V = String}