Question:
As I'm working on a Hindley-Milner typed lambda calculus, in order to make it usable I need to add some types such as list and pairs. The way I currently do it is, I have an unsafe keyword that lets me explicitly set the type of a global function that tells the type checker to just trust the explicitly given type and ignore the term's type. Then I use Church encoding to encode my types, so for instance, I can create my Pair type by encoding it in a (a -> b -> x) -> x function like this:
unsafe pair : a -> b -> (Pair a b) = \a.\b.\f.(f a b)
unsafe pairRead : (a -> b -> x) -> (Pair a b) -> x = \f.\p.(p f)
Then I can define fst and snd like:
fst = (pairRead \a.\b.a)
snd = (pairRead \a.\b.b)
It seems that, since lambda calculus is Turing complete and I'm just wrapping lambda types with explicitly given types, I should be able to emulate any Algebraic data types, and more, in case ADTs have any limitations (seems like they do since there are also GATDs, which I guess I should also be able to emulate).
The obvious problem is that this is not type safe, which defeats the whole purpose of type checking, so I wonder if there is already a way to do this in a safe manner instead of attempting to recreate the wheel. I could also just implement ADTs but, if there's a way to make it safe, I'd like to use this better since it's closer to what I have already implemented, it's simpler (I won't need to also implement pattern matching) and it seems to be a superset of ADTs.
What I've done so far:
I'm pretty sure if I provide a way to encode an existing type into a custom type while keeping all the type variables, and a way to go back to the original type, then I will be safe.
For instance, I could add a keyword using that uses this syntax:
using [CustomTypeName] [FullListOfTypeVariablesInOriginalType] = [OriginalType] {
[FunctionsDefinitions]
}
Inside [FunctionsDefinitions] I'd define my functions and I'd have access to two other new keywords $to and $from, which would have the types of functions that go from the original type to the custom type, and the other way around, respectively, but would behave as an identity function during evaluation. So for instance, I would define my pair functions like this: (note that I'm including the x in the Pair definition):
using Pair a b x = (a -> b -> x) -> x {
pair = \a.\b.($to \f.(f a b))
pairRead = \f.\p.(($from p) f)
}
In this case, $to and $from would be equivalent to these functions (defined using the unsafe keyword I mentioned above):
unsafe $to : ((a -> b -> x) -> x) -> Pair a b x = \x.x
unsafe $from : Pair a b x -> ((a -> b -> x) -> x) = \x.x
So this should be safe since $from will always map back to the original type because the Pair type includes every type variable in the original type, but is still not good.
Since I'm including x in the definition of Pair, my Pair type will include the return type of whatever function I pass to pairRead. So if at any point I read a pair p using pairRead with a function that returns a number, from that point on I could only read pair p using functions that return numbers, since the x in Pair would have become a number type. For instance, a function swap = \p.(pair (snd p) (fst p)) would require both types in the pair to be the same.
So I'd like to be able to ditch the x in the original type to get Pair a b. So the question would be, when can a variable be safely ditched? I think this would be variables that are not bound to an outer type. In my definition of pair above, the type of \f.(f a b) is really $\forall x (a \rightarrow b \rightarrow x) \rightarrow x$ with $a$ and $b$ bound to the outer type, so if I want to encode this type, I only need to store the types of $a$ and $b$ to be able to recreate the original type.
I think what my type checker needs to do is basically (in the case of Pair), when it sees a $to keyword, first type check its term, then unify its type with (a -> b -> x) -> x (using a fresh copy of x) and finally make sure that no occurrence of x has been unified with any type that exists in the current type context. If that's all good, then return the type Pair a b with a and b taken from the resulting type.
But then again, I'm no mathematician and I don't have a proof of correctness, and somebody may have already came up with a better way to do this.
