Higher Logics

I've written about quite a few irritations of C#/CLR, including asymmetries in CIL , oddly unverifiable CIL instructions , certain type constraints are forbidden for no reason , delegate creation bugs , the lack of higher-kinded types , equality asymmetries between events and IObservable , generics/type parameter problems , lack of usable control over object layouts , and just overall limitations of the CLR VM . I've just smack into yet another annoying problem: type parameter unification is forbidden . The Microsoft Connect bug filed in 2004 was closed as By Design . Here's a simple code fragment demonstrating the problem: class ObserveTwo<T0, T1> : IObservable<T0>, IObservable<T1> { } This will fail with the error: 'ObserveTwo<T0,T1>' cannot implement both 'System.IObservable<T0>' and 'System.IObservable<T1>' because they may unify for some type parameter substitutions This is frankly nonsense. What's

A recent discussion on LtU brought up a common limitation of modern languages and runtimes. Consider some set of abstractions A, B, ..., Z that we wish supported some custom operation Foo(). Languages like C# give only two straightforward possibilities: inheritance and runtime type tests and casts. Inheritance is straightforward: we simply inherit from each A, B, ..., Z to make A_Foo, B_Foo, ..., Z_Foo, with a custom Foo() method. Unfortunately, inheritance is sometimes forbidden in C#, and furthermore, it sometimes prevents us from integrating with existing code. For instance, say we want to integrate with callback-style code, where the existing code hands our program an object of type A. We can't call Foo() on this A, because it's not an A_Foo, which is what we really wanted. This leaves us with the undesirable option of using a large set of runtime type tests. Now type tests and casts are actually pretty fast , faster than virtual dispatch in fact, but the danger is i