The Hugs98 interpreter has been extended with features which lets you instantiate and use .NET objects from within Haskell, and vice versa Hugs98 for .NET takes a hands-off approach, providing 'just' the ability to interoperate well with .NET. That is, it does not try to compile Haskell into .NET's IL and have the .NET run-time execute it. Instead the Hugs98 interpreter operates side-by-side with the .NET run-time
So why is the restriction imposed? The reasoning behind it is fairly subtle, and is fully explained in the Haskell 98 report. Basically, it solves one practical problem (without the restriction, there would be some ambiguous types) and one semantic problem (without the restriction, there would be some repeated evaluation where a programmer might expect the evaluation to be shared). Those who are for the restriction argue that these cases should be dealt with correctly. Those who are against the restriction argue that these cases are so rare that it's not worth sacrificing the type-independence of eta reduction.
A witness is a value that witnesses some sort of constraint on some list of type variables. This library provides support for simple witnesses, that constrain a type variable to a single type, and equality witnesses, that constrain two type variables to be the same type. The library also provides classes for representatives, which are values that represent types.
The Curry-Howard correspondence is a mapping between logic and type systems. On the one hand you have logic systems with propositions and proofs. On the other hand you have type systems with types and programs (or functions). As it turns out these two very different things have very similar rules. This article will explore the Curry-Howard correspondence by constructing a proof system using the Haskell type system (how appropriate since Haskell is named after Haskell Curry, the "Curry" in "Curry-Howard"). We'll set up the rules of logic using Haskell types and programs. Then we'll use these rules as an abstract interface to perform some logic profs.