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

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

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

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

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

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

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

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

	;; 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]))