After finalizing some of my idea prototypes in Ωmega, I intend to port a part of the code to Haskell, to enjoy the speed advantages of a compiled language.
Unfortunately Haskell does not support user-defined kinds, so I was wondering how to simulate them at least, in order to get some confidence that my type-level constructs do not drift into no-no-land.
This literate haskell file demonstrates how I put instance constraints to work, and thereby define the inference rules for well-kinded phantom type indexes. I am sure somebody has already done this, I would like to hear about it. Anyway, this almost allows me to introduce Ωmega's checked singleton types in Haskell.
Sadly GHC does not yet allow instance definitions for type families, but it would be cool if somebody could provide me a workaround.
Subscribe to:
Post Comments (Atom)
5 comments:
Brent Yorgey and the usual suspects are working on a mechanism for lifting usual data type declarations to the kind level. You might give them a ping about it.
Alas, defining instances on type families is unlikely to happen because it's not clear how it could even work.
Type families are open functions on types, type classes alone are open functions from types to terms. Both are distinguished from their parametric equivalents (type constructors and polymorphic types, roughly) by inspecting their arguments in a manner similar to pattern matching. The type variables bound by the "patterns" can then be used to construct the result.
So, to define an instance for a type family as you'd like to do is essentially using function application in a pattern match; an instance for some type "Foo a" where Foo is a type family means taking a type "t" and reconstructing a type "a" such that "Foo a ~ t". Given that type families, like term-level functions, are not required to be injective, this is clearly impossible in the general case.
Anyway, if your goal here is to ensure that only terms with valid types are constructed, you should be fine; the problem is that you may have to spend more time than you might prefer holding GHC's hand while doing so. If you want to ensure that intermediate computations done at the type level are valid in ways not reflected by terms, I'm not sure your approach here is really workable.
I can't really offer further suggestions without knowing more about what you're trying to accomplish and what your tolerance for annotations rather than inference would be.
Thanks for the insightful stuff! Yes I just want to trick GHC into propagating class constraints when the (Plus m n) type expression cannot be reduced to type constructors, e.g. when type variables are involved. If it can, the instance declarations regarding Z and S will kick in anyway.
In end effect I want to declare types like this:
plus :: (Nat a, Nat b) => Nat' a -> Nat' b -> Nat' (Plus a b)
Ok. I thought you might be after something like that. If your ultimate goal is using type-level functions to calculate the correct type of a term-level function, where the type arguments are derived from the types of the term arguments, you'll need to use a type class function somewhere in there to recover a term-level result from the type-level result. Further, if the function you need is recursive, you'll probably need to implement that recursion through the type class.
In some circumstances using GADTs can actually work against you here, because it conceals the type class constraints inside the constructor, which makes it more awkward to get access to those constraints for the purpose of type-level computation.
That said, in cases where the type-level result fully determines the term-level result, you can take a shortcut by using a general "get the term for this type" approach.
If you'd like to see worked examples of the above, here's a demonstration of both recursion via a type class, and getting unique term results from a type-level calculation.
...after some research...
Recently proposed constraint families might help.
But the simplest solution may be indeed to wait till proper user-defined kinds become available in haskell.
Post a Comment