[Haskell-cafe] Typing Judgments for Haskell2010++

[Shayan Najd Javadipour]

Hi Haskell Cafe!

To develop Haskell-Type-Exts (HTE) [1,2], I need to have typing judgments
for each language construct in Haskell 2010 with two extensions: RankNTypes
and local assumptions (GADTs, Type Functions and etc). Since I could not
find any academic paper describing a type system supporting both local
assumptions [3] and RankNTypes [4], we tried to combine the two systems. We
also tried to extend the type system to support Patterns and some other
constructs. The result (in a very sketchy state) is posted at:
  http://cleantypecheck.wordpress.com/2012/06/06/typing-judgment-rules-14/

Now before I start to implement these rules in HTE, I need to make sure of
their validity. Therefore, I'd highly appreciate if experts would take a
closer look at these judgement rules and comment.

Considering the fact that HTE is a Google SoC project and me being just a
motivated student (limited knowledge/experience), the success of this
project strongly relies on Haskell community's support.

Thanks!

/Shayan

[1]
http://www.google-melange.com/gsoc/project/google/gsoc2012/shayannajd/18001
[2] http://cleantypecheck.wordpress.com/2012/05/03/kickoff/
[3] D. Vytiniotis, S. Peyton Jones, T. Schrijvers, M. Sulzmann.
OutsideIn(X) – Modular type inference with local assumptions
[4] S. Peyton Jones, D. Vytiniotis, S. Weirich, and M. Shields. Practical
type inference for arbitrary-rank types.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120606/c7d80b56/attachment.htm>