Very interesting writeup! Thanks. This now gives me more ideas to use in the language I'm working on.
I independently had what seems to be a similar idea, which is sort of like "anonymous type classes." For example, Vectors, Lists, Strings, Maps, Sets, etc all have something like a "size" function. So say there exist functions like
size : Vector a -> Int
size : String -> Int
size : List a -> Int
...
And say we wanted to make a function like:
show_size a = show a + " has a size of " + show (size a)
To write this in Haskell, you'd have to create a `Size` type class:
class Size a where size :: a -> Int
And then write instances for all of them. And you'd have to do the same for `show`. But that's almost as tedious as the Java example. Now a Haskell type class is essentially a set of named function signatures, so instead, you can create a type class "on the fly":
show_size : a of {size: a -> Int, show: a -> String} -> String
The cool thing here is that you keep the type information, in a similar way to what you were describing:
foo : a of {f: a -> b -> Int} -> b of {g: b -> Int -> b} -> b
foo a b = g b (f a b + 10)
So here we know that as long as there exist appropriate `f`s and `g`s, then we can pass any `a` and any `b` in and get a `b` back.
I independently had what seems to be a similar idea, which is sort of like "anonymous type classes." For example, Vectors, Lists, Strings, Maps, Sets, etc all have something like a "size" function. So say there exist functions like
And say we wanted to make a function like: To write this in Haskell, you'd have to create a `Size` type class: And then write instances for all of them. And you'd have to do the same for `show`. But that's almost as tedious as the Java example. Now a Haskell type class is essentially a set of named function signatures, so instead, you can create a type class "on the fly": The cool thing here is that you keep the type information, in a similar way to what you were describing: So here we know that as long as there exist appropriate `f`s and `g`s, then we can pass any `a` and any `b` in and get a `b` back.