lexi-lambda
Alpha conversion in infer/check
In https://github.com/ollef/Bidirectional alpha conversion is done in the inference/checking of lambdas. You don't do that and just add the assumption to the context. Won't this mean that the following will fail, since multiple assumptions with the same variable will be in the context:
(\x -> (\x -> x)) () ()
Yes, this is an issue I am aware of. It’s one I was originally disinclined to fix because my ulterior motive for this implementation was to implement this in Racket, which does not suffer from this issue due to identifier hygiene. A fix probably wouldn’t be that hard, but this implementation is also just a tool to demonstrate the paper in as simple a way as possible, and I’m reluctant to complicate the implementation much more than it already is.
Oh okay, I see. In the paper they don't even mention this issue with identifiers as far as I know. I do wonder what happens if you just add multiple assumptions with the same identifier to the context and always just take the last one (removing the well-formed constraint for it). I don't see any issues arising from it so far, but I will experiment with it and see.
Are you planning to implement the follow up paper also (http://www.cs.cmu.edu/~joshuad/papers/gadts/)? Sadly I am unable to find any implementations of it.
Are you planning to implement the follow up paper also (http://www.cs.cmu.edu/~joshuad/papers/gadts/)? Sadly I am unable to find any implementations of it.
Maybe eventually, but at the moment, probably not. It’s considerably more complex than the paper this repo implements, and it’s not immediately useful for my main project, Hackett. I will eventually want GADTs, though, so maybe I’ll try and implement it then.
I do wonder what happens if you just add multiple assumptions with the same identifier to the context and always just take the last one (removing the well-formed constraint for it). I don't see any issues arising from it so far, but I will experiment with it and see.
I haven’t encountered any issues with this modification in some code I’ve been working on that’s based on this repo. The only risk I’ve seen of doing it this way is that if you have a bug elsewhere whereby a variable isn’t added to the context properly, but there’s another one in scope by the same name, it can manifest in strange ways when the wrong type is retrieved. It’s also not terribly complex to use the implementation as-is and just do renaming on the frontend.
