Higher Logics

The CLR's lightweight code generation via DynamicMethod is pretty useful, but it's sometimes difficult to debug the generated code and ensure that it verifies. In order to verify generated code, you must save the dynamic assembly to disk and run the peverify.exe tool on it, but DynamicMethod does not have any means to do so. In order to save the assembly, there's a more laborious process of creating dynamic assemblies, modules and types, and then finally adding a method to said type. This is further complicated by the fact that a MethodBuilder and DynamicMethod don't share any common interfaces or base types for generating IL, despite both of them supporting a GetILGenerator() method . This difficulty in switching between saved codegen and pure runtime codegen led me to add a CodeGen class to Sasa, which can generate code for either case based on a bool parameter. Since no common interface is available for code generation, it also accepts a delegate to which it dispa...

Most abstractions of interest have a natural dual, for instance, IEnumerable and IObservable, induction and co-induction, algebra and co-algebra, objects and algebraic data types, message-passing and pattern matching, etc. Programs are more concise and simpler when using the proper abstraction, be that some abstraction X or its dual. For instance, reactive programs written using the pull-based processing semantics of IEnumerable are far more unwieldy than those using the natural push-based semantics of IObsevable. As a further example, symbolic problems are more naturally expressed via pattern matching than via message-passing. This implies that any system is most useful when we ensure that every abstraction provided is accompanied by its dual. This also applies to virtual machine instruction sets like CIL, as I recently discovered while refining my safe reflection abstraction for the CLR. A CIL instruction stream embeds some necessary metadata required for the CLR's correct opera...

I've lamented here and elsewhere some unfortunate inconveniences and asymmetries in the CLR -- for example, we have nullable structs but lack non-nullable reference types, an issue I address in my Sasa class library . I've recently completed some Sasa abstractions for safe reflection, and an IL rewriter based on Mono.Cecil which allows C# source code to specify type constraints that are supported by the CLR but unnecessarily restricted in C#. In the process, I came across another unjustified decision regarding verification: the jmp instruction . The jmp instruction strikes me as potentially incredibly useful for alternative dispatch techniques, and yet I recently discovered that it's classified as unverifiable. This seems very odd, since the instruction is fully statically typed, and I can't think of a way its use could corrupt the VM. In short, the instruction performs a control transfer to a named method with a signature matching exactly the current method's si...

Awhile ago, I had posted about an embedding of a stack language in C#. The type signatures of the functions and the stack object encoded the consumption and production of stack values, so if your program compiled, it ran correctly. Unfortunately, the prior structure had a safety problem when generating code which I noted, but didn't have time to address. The new structure provided below does not have the safety problem, and any functions that compile are guaranteed to execute correctly. I have also altered the style to emphasize the row variable representing the "rest of the record" which the operation knows nothing about. The row variable is denoted by "_". This is still a fairly limited embedding, but I have added a few convenience functions, and may yet add more. Here is a sample program: var d = new DynamicMethod("test", typeof(void), null); var s = 1.Load() // load constant: { int } .Int(2) // load constan...

Parametric polymorphism is a powerful tool for constructing and composing safe programs. To demonstrate this, I've constructed a tiny embedded stack language in C#, and I exploited C# generics, aka parametric polymorphism, to ensure that any embedded programs are type-safe, and thus, "can't go wrong". Moreover, this language is jitted, since I use ILGenerator of System.Reflection.Emit, and the complexity of doing this was no higher than creating an interpreter. This is mainly because the CLR is itself a stack-based VM, and so jitting a stack-based program to a stack-based IL is fairly natural. Here is the type-safe representation of the stack: public struct Stack<R, T> : IDisposable { internal ILGenerator gen; public Stack(ILGenerator gen) { this.gen = gen; } public void Dispose() { this.Return(); } } This type encapsulates the IL output stream and uses two phantom type variables to encode the values at the top of the ...