API function to check whether one type fits "in" another
simonpj at microsoft.com
Fri Jun 29 18:00:03 CEST 2012
If you develop a function that does what you want, and want to make it part of the GHC API, we'd definitely consider including it. But I don't want to promise to develop something just for you; I'm just too snowed under with other stuff.
I really think the "holes" that Thijs is working on might be good for you. He has a prototype already I think.
| -----Original Message-----
| From: "Philip K. F. Hölzenspies" [mailto:pkfh at st-andrews.ac.uk]
| Sent: 28 June 2012 11:11
| To: Simon Peyton-Jones
| Cc: thijsalkemade at gmail.com; glasgow-haskell-users at haskell.org
| Subject: Re: API function to check whether one type fits "in" another
| Dear Simon, et al,
| Thank you very much for your reply. Some of the pointers you gave, I wouldn't
| have come across, for not knowing to have to browse through the module Inst, for
| I read the OutsideIn paper (JFP), but that's a fair while back. I was pointed to
| Thijs's work in progress at an Agda talk recently. The front-end we're working on
| should be portable to any lambda-language with strong types, so the availability
| of holes in Agda and Idris makes the implementation for those back-ends a
| There is one limiting consideration, however: We want to get this up and running
| the next few weeks and we would like to keep things in-sync with the
| developments on the different back-ends. This is why I'm trying to stay as close
| as possible to the more "public" API parts (the things that are documented and
| haven't changed significantly since at least 7.0.4).
| In this light, I was wondering whether it's not worth having a function that does
| all this plumbing in the API that is persistent through future versions, much like
| pure interface to the parser (GHC.parser). Preferably it would look something like:
| :: DynFlags -- the flags
| -> FilePath -- for source locations
| -> Type -- expected
| -> Type -- actual
| -> Either
| The implementation would have to make sure the pre-conditions of the type
| arguments are met. Is this worth pursuing? Would be a significant amount of
| work? Am I being pushy if I make this a feature-request?
| PS. I'm going to study the Trac you pointed to in more detail; browsing it was
| already a learning experience about the whats and wheres of the GHC API.
More information about the Glasgow-haskell-users