| 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; |
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
| -- 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} |
| (* 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: |
| (ns overtone-playground.heart-murmur | |
| (:use overtone.core | |
| overtone.inst.sampled-piano | |
| overtone.samples.piano)) | |
| ;; (boot-server) | |
| ;; (sampled-piano) | |
| ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; Reproducible randomness |
