Are higher-kinds in C# real?

In a recent Twitter semi flame-war I encountered some opposition to the idea that the approach to higher-kinds used in language-ext is a valid approach. In the end I decided to back out of it, because nothing is solved on Twitter, but I felt I needed to add enough context so those who follow me on Twitter can at least judge for themselves.

In this article I want to prove that f a in Haskell is equal (up to isomorphism) with K<F, A> in C#.

To do this we need to build our own type system. It needs to follow the extended lambda calculus approach used by the likes of Haskell and other FP languages. Then, we need to augment it, so that we can represent generic-types the way that C# does it. If we can transform Haskell style higher-rank polymorphic representations to C# generics and back again (without losing any fidelity), we have a proof.

To make a simple type system we need:

• Primitive types (int, string, etc.)
• Type variables (like the A in Option<A>)
• Type names (like the Option in Option<A>)
• Lambda abstractions
• Type applications

The last two items need a little explanation...

Lambda abstractions are like lambdas in any programming language except they're in the type system and are 'run' at compile time. The 'running' of the lambdas should (by the end of the compilation) generate concrete types. Lambda abstractions follow lambda calculus in that they accept single arguments only. Multiple arguments are achieved by nesting multiple lambdas.

Type applications are what's used to invoke the lambda abstractions (passing an argument to evaluate). They can apply a single argument to a single lambda. So applying multiple arguments to nested lambdas needs multiple type applications. This also means you can partially apply arguments. By example: Option<int> is applying the int type to the Option lambda-abstraction.

First, we need a base type: Ty:

public abstract record Ty;

Then a primitive type to define all the supported primitives:

public enum Prim
{
    Int,
    String,
    Bool
}

public record TyPrim(Prim Value) : Ty;

Type variables:

public record TyVar(string Name) : Ty;

Type names for concrete types:

public record TyName(string Name) : Ty;

Lambda abstractions:

public record TyLambda(string VarName, Ty Body) : Ty;

You should recognise the pattern from lambdas in languages that support them: a letter defining the variable-name of the argument and a body-expression. The idea is that when an argument is applied to the lambda the instances of TyVar(VarName) in Body are replaced with the applied type.

Type application:

public record TyApply(Ty LamdbaAbs, Ty Arg) : Ty;

The first argument should evaluate to a TyLambda and the second argument is the value to pass to the lambda as its parameter.

We can also make construction of these types a little easier by adding some static functions to Ty:

public record Ty
{
    public static readonly TyPrim Int = new(Prim.Int);
    public static readonly TyPrim String = new(Prim.String);
    public static readonly TyPrim Bool = new(Prim.Bool);
    public static TyVar Var(string name) => new(name);
    public static TyName Named(string name) => new (name);
    public static TyLambda Lambda(string varName, Ty body) => new(varName, body);
    public static TyApply Apply(Ty lambda, Ty arg) => new(lambda, arg);
}

That's all of the basics we need for the moment.

So, something like f a in Haskell would (in its type-system) look like this:

Ty.Apply(Ty.Var("f"), Ty.Var("a"))

Which, when evaluated, will look up f (which it expects to be a TyLambda) and then substitute the evaluated a for VarName in the lambda body. And so, this is how Haskell (and most FP languages) does polymorphism (generics). C# doesn't represent generic types as lambdas, which presumably is why higher-rank polymorphism isn't a thing in C#.

Let's take a look at my solution for higher-rank polymorphism in C#. It is primarily enabled by a single type: K<F, A>. My argument is that K<F, A> is equal up to isomorphism to f a in Haskell.

What does "equal up to isomorphism" mean? It means there's a way of transforming one type to the other type and back again without losing any fidelity. So, they're not equal because they're made of different components, but they're convertible back'n'forth and so they're equal up to isomorphism. Which is a slightly weaker statement about equality, but they're functionally equal because we can make one from the other.

K<F, A> can't be directly represented with the type-system we have created. Let's ignore the K part – it is genuinely irrelevant to this discussion, it's just a label – there are no members in the K type, so the only thing that matters is the <F, A> part. The <F, A> part is a tuple of types. So, let's add TyTuple to our type system:

public record TyTuple(Seq<Ty> Items) : Ty;

A tuple is zero or more types. Let's have some friendly constructors functions in Ty:

public static TyTuple Tuple(Seq<Ty> items) => new (items);
public static TyTuple Tuple(params Ty[] items) => new (toSeq(items));

We can now represent K<F, A> or really <F, A> in our type system:

Ty.Tuple(Ty.Var("f"), Ty.Var("a"));

So, to prove the isomorphism between f a and <F, A> we need to be able to convert between their type-system representations without losing anything in the process.

Let's create a K type as it is in C# (I'm using Option<int> to make it a bit more interesting):

var kOptionInt = Ty.Tuple(Ty.Named("Option"), Ty.Int);  // Option<int>

From that, can we create the Ty.Apply version? Yes, we can...

var optionInt = Ty.Apply(kOptionInt.Items[0], kOptionInt.Items[1]);

To prove the isomorphism we need to back able to go back and prove the types are the same...

var kOptionInt2 = Ty.Tuple(optionInt.LamdbaAbs, optionInt.Arg);

Console.WriteLine(kOptionInt == kOptionInt2); // True

It outputs True and so proves we can convert one way and back again. Let's, for completeness, start with Ty.Apply and convert to Ty.Tuple and back again:

var optionInt = Ty.Apply(Ty.Named("Option"), Ty.Int);
var kOptionInt = Ty.Tuple(optionInt.LamdbaAbs, optionInt.Arg);
var optionInt2 = Ty.Apply(kOptionInt.Items[0], kOptionInt.Items[1]);

Console.WriteLine(optionInt == optionInt2); // True

That also outputs True – they're equal up to isomorphism and we've proved it.

To take this proof further we can build the evaluator for the types and prove that the evaluated types are equal (up to isomorphism). I will do that if this article gets some push-back, but I already know the answer.

So, it doesn't matter what the purists say. The language-ext approach to higher-kinds is the same as the approach in Haskell and any other language with higher rank polymorphism. Yes, we need an additional type to represent the partially applied type (for example, IO for the IO<A>), but that doesn't matter as we only attach the trait implementation to that 'partially applied' type. That's not much different to having separate types for the class instance definitions in Haskell – in fact I'd argue they're also isomorphic.

I do feel there's often a snobbishness about those of us who are doing functional programming in C#. The arguments are nearly always based around some bullshit academic reasoning not related to solving the problem but purely to be a position to sneer from. It adds nothing. Or we get something like "why do it in C# in the first place, when there are better languages around?" – which is always a naive statement to make.

By the way, I have no issue with academics or the pursuit of knowledge through academia. The whole of language-ext is standing on academic shoulders. But the unwillingness to accept other practical solutions to problems and then the inevitable sneering is tiring and unnecessary. C# can achieve every aspect of higher-kinded traits using its type-system. No hacks, no reflection, no dynamic references. Purely with its type-system – that should be the end of the discussion.

Haskell (the poster-child for pure functional programming) has many problems also. I led a team doing a pure Haskell project two years ago. It was the first time I'd used Haskell in a professional setting – I've used it on and off for many years on personal projects, just never professionally. The major problems I encountered were:

• The open-source library ecosystem is poor:
  • Lots of unmaintained and incomplete projects for critical functions
  • Lots of amateurish solutions (again, for critical functions) – I put this down to the Haskell world being full of academics and not professional engineers.
  • We ended up building our own libraries of things you'd normally take off-the-shelf in other ecosystems. As a leader seeing time eaten up this way is tough.
• The more junior devs in my team had a really hard time with the language. These devs had worked with language-ext for years, so it's not like they had no exposure to pure functional programming, but for some reason they struggled. In parallel to this we'd even done a weekly 'Haskell book club' to get everyone up to speed and to encourage discussion – but it didn't really move the needle.
• The tooling, although much better than it was when I first learned Haskell, is still poor. The compiler is slow. It tends to exit on the first error and then produce other spurious errors. The debugging story was extremely poor (I suspect this was the main issue for juniors struggling). Even random things like the auto-formatting engine we were using just stop being supported. And the plugins to VSCode seem to be endlessly buggy.

Luckily, as a co-founder of the company, I was able to weather the relatively slow progress of the project: I understood that the code was likely to be more robust and would need less maintenance and so a slower initial phase of the project could be caught up later.

However, after a year we decided to can the project. It was a business decision not related to Haskell, so I won't claim it was the cause of the canning, but based on my experience I will probably never start a greenfield project with Haskell again.

Don't get me wrong, I still love the language, it has directly influenced much of language-ext, but the ecosystem is weak – which, after 30 years of Haskell's existence, probably means it's not likely to get much stronger.

The reality is C# is used by more people than Haskell. The library ecosystem is mature. C# for all its problems has world-class tooling. The compiler is probably second to none. The IDEs (Visual Studio or Rider) are second to none. There are probably more people doing functional programming in C# than in the entire Haskell community. These are things to not take lightly when choosing a language to build substantial projects with.

Don't we deserve higher-kinds? Aren't we allowed to follow the pure functional programming paradigm?

I think we are.

As expected a flame war started as soon as I posted this to Twitter (I mean, like within minutes!)

Anyway, I'm opting out again, because the arguments are circular and going nowhere. But, the whole point of this post was to ease the mind of those stepping into this world for the first time – it wasn't to make lambda calculus obsessives happy. So, I'll cover some of the "issues" raised and then leave it as that:

1. "As for your proof, here is a simple counter-example. In C# the following instantiation of type variables is legal: K<String, Int>. In Haskell 'String Int' fails to type check (exactly because there is simply no notion of kinds in C#)"

There are kinds in C#, we have generics, so we have kinds – we just can't use type-variables as the first part of the * -> * arrow (meaning we can't parameterise the F in F<A>).

K<string, int> is legal in C# but it has no use for implementing traits. That doesn't make the approach invalid. The argument that it should be invalid is arguing that the first parameter (string) should be a lambda-abstraction. But it doesn't need to be in the tuple based approach to implementing higher-kinds, because we're not using lambda-abstractions, and we're not using lambda-abstractions because we're using tuples, ... So, the argument is a pointless circular one. It's basically saying "It's not implemented like Haskell, therefore it's not valid" which isn't a good argument.

However, stating that IO as the first argument (for example) is a * -> * kind in Haskell and a * kind in C# does require a little more explanation. The isomorphism works in the type-system I invented in this article. The isomorphism doesn't work in Haskell or C# – Haskell doesn't have tuple types and C# doesn't have lambda-abstractions – so this proof can't be run in either language.

My primary point with the proof above was that a 2-tuple and a type-application are isomorphic.

I realise that's not the most profound proof to ever be written, but it validates the approach of using the tuple-type K<F, A> to represent F<A>. F isn't a lambda-abstraction because it doesn't need to be in our approach, we are able to resolve the relevant trait from the * type without the need for a partially applied value being passed as an argument to a trait-type.

Quite simply, we don't need lambda-abstractions to implement higher-kinded traits, which is lucky, because C# doesn't have them.

2. "No, Haskell does not encode HKTs. Its type system is directly based on lambda calculus, and LC is _the_ definition of kinds and types. There is no need to encode the definition when you (Haskell) are the "native" implementation of the definition."

I love it when someone points out Haskell's implementation is done with lambda calculus as I state clearly in the article and I implemented the type-system using it! Some people just like to score points on the internet I guess. Perhaps it needs a new term: 'Lambdasplaining' maybe?

3. "We can indeed see this HKT embedding as an alternative implementation, only in library space and not in the type system. It is not the same or equivalent to native support though and claim that C# supports HKTs."

This is one of those "you can't play with your toys because they're not as good as ours" arguments. It looks down on the implementation saying it's not 'native'. The only thing language-ext does is say: "Let's use this type K<F, A> to represent higher-kinds" – but K<F, A> is still a C# type, it's not something magical hacked into the type system – it introduces a convention, sure, but that's it. Everything else is the C# type-system as-is. There's no reflection, there's no cheating, all constraints are enforced by the C# type checker. As it should be. F is not constrained to be a lambda-abstraction, because lambda-abstractions don't exist and we don't need them to implement higher-kinded traits.

4. "As you write yourself, C# allows and accepts only type variable of kind *. In particular not of kind * -> *. No arrows, no HKTs. This is the definition of what it means to be a HKT and you can't promote an embedding to the real thing just by declaring them as equivalent."

This argument is, yet again, arguing that only lambda-abstractions can encode higher-kinded types. Yet, as we see, they can be encoded by other means. The general crux of this poster's recursive responses is that "it's not lambda calculus, so your approach isn't valid".

My response is this: Alan Turing proved that his Turing Machine was equivalent to Lambda Calculus. So, not every implementation has be in Lambda Calculus to be valid. And, if you have a problem with that, take it up with Alan Turing.

Response from Erik Meijer

"Super cool hack, really; but an encoding does not imply it is usable. More importantly

> Don't we deserve higher-kinds? Aren't we allowed to follow the pure functional programming paradigm?

Higher kinds does not give you pure functions

https://queue.acm.org/detail.cfm?id=2611829…

If you are using C#, IMHO, it is best to stick with idiomatic C# instead of trying to bolt a pseudo Haskell style on top.

Don't fight the language, embrace it. Write baby code. KISS."

I have a lot of respect for Erik. He brought LINQ to C# after all! He's one of the few people in the industry that I am always interested in hearing from, because even though his Twitter handle is @headinthebox, he really is someone who thinks outside of the box. I would encourage you to look up his talks on YouTube as they're always thought provoking and usually pretty inspirational too.

That doesn't mean I agree with him on everything though!

Before Erik wrote this response I already knew his position on this (because I've watched his talks). But let's break down what he's said:

but an encoding does not imply it is usable

Nobody knows yet whether this will be usable, because I have yet to release language-ext v5. But, I've been dog-fooding it myself, building a DB Layer for Foundation DB and I have to say, it feels pretty good! The fact that this actually makes LINQ work like do notation in Haskell (i.e. once you implement the Monad<M> trait for your type, LINQ starts working), in my mind, finishes the job that should have been done by the C# team. They stopped short of implementing monads in C# properly and instead opted for 'magic methods' (Select and SelectMany) – this was a colossal mistake in my humble opinion. They should have at least committed to making a trait system to deal with the C# magic methods (all of them) if they weren't able to do it at the time.

Higher kinds does not give you pure functions

That wasn't what I was implying with the sentence I wrote. So a small misunderstanding there.

https://queue.acm.org/detail.cfm?id=2611829…

I'd previously read 'The Curse of the Excluded Middle' stating that "Mostly functional" programming doesn't work. Mostly.

I agree with the basic premise and go to great lengths in the Monad article to emphasise the importance of everything being pure functions. However, I don't fully agree with Erik's position.

Let's say this was my program:

void Main()
{
   PureFunction().Run();
   ImpureFunction();
}

If those functions represent (by some odd coincidence) half of your code base each (half pure, half impure). Then you still benefit from the pure functional programming half. So, you can start small and build up something that becomes progressively more stable. Every block of pure code, even if surrounded by impure code, is one block you don't have to worry so much about. Is it fundamentalist programming? Of course not. But slowly building out from there pays you back each time you expand the scope of the pure code. You won't have solved all of the worlds ills, but you've made part of the world's ills better. Any pure function in an impure code-base is, by-definition: more robust, easier to compose, cacheable, parallelisable, etc. these are real benefits, doesn't matter how small you start.

I have direct experience of this, the project I ran from 2005 - 2023, which was a 10 million lines of code behemoth, started out imperative and OO. It kept falling foul of the issues you get all of the time with mutable-state imperative applications (we were writing 'baby code' as Erik calls it). I looked for an alternative approach and that birthed language-ext. Over time language-ext took over the application.

Still today there are areas that are not pure, but there's a huge amount that is, and that code is easier maintain and extend than the impure parts. So, you do get benefits, and you can progressively move over to pure FP. Just remember, any impure function in a pure expression makes the whole thing impure – so as devs we have to be strict with ourselves.

But, even in a language like Haskell there's a function called unsafePerformIO which breaks all of the purity guarantees of Haskell – it doesn't show up in any function type-signature – so you have no idea whether any of your code is pure. By convention, people try not to do that, but they can. It's the same in any other language, you have to be strict with yourself. And, on a team, you have to have a good code-review process in place so impure code doesn't sneak into the pure bits of your code. It requires a culture change within your team, everyone needs to understand why you're doing this.

Ultimately though, that's why language-ext is more of a 'base class library' for FP in C#. Because if you're going to do pure FP in C# then you're not going to get it by just adding an Option library to your app, you have to go all-in. This library is intentionally breaking the idioms of C# to create a new community of functional-programmers within the C# set of devs. Much like the sub-communities with Scala-land (although, hopefully without the infighting!)

If you are using C#, IMHO, it is best to stick with idiomatic C# instead of trying to bolt a pseudo Haskell style on top.

As I've mentioned, I'm breaking the idioms on purpose, there's room for two. But, even with that said, I think the idioms of C# have moved quite far from where it was in v1.

Look at the new INumber type (which is the base interface for Int32 etc.):

  public interface INumber<TSelf> : 
    IComparable,
    IComparable<TSelf>,
    IComparisonOperators<TSelf, TSelf, bool>,
    IEqualityOperators<TSelf, TSelf, bool>,
    IModulusOperators<TSelf, TSelf, TSelf>,
    INumberBase<TSelf>,
    IAdditionOperators<TSelf, TSelf, TSelf>,
    IAdditiveIdentity<TSelf, TSelf>,
    IDecrementOperators<TSelf>,
    IDivisionOperators<TSelf, TSelf, TSelf>,
    IEquatable<TSelf>,
    IIncrementOperators<TSelf>,
    IMultiplicativeIdentity<TSelf, TSelf>,
    IMultiplyOperators<TSelf, TSelf, TSelf>,
    ISpanFormattable,
    IFormattable,
    ISpanParsable<TSelf>,
    IParsable<TSelf>,
    ISubtractionOperators<TSelf, TSelf, TSelf>,
    IUnaryPlusOperators<TSelf, TSelf>,
    IUnaryNegationOperators<TSelf, TSelf>,
    IUtf8SpanFormattable,
    IUtf8SpanParsable<TSelf>
    where TSelf : INumber<TSelf>

The .NET team, in their own especially wordy style, are also using this trait technique. With IAdditiveIdentity and IAdditionOperators they are also embracing semigroups and monoids! So, I'm not sure this approach is really that far away from idiomatic C# any more.

Of course, taking this a step further to implement more complex types like Monad and Applicative could be argued to be pushing that boundary a little, but the technique is the same really.