0

Given the following type family:

type family C a b :: Constraint

This has type:

 C :: * -> * -> Constraint

Whilst C Int is invalid (one can not partially apply a type family).

We can write the following:

class (C a b) => C' a b 
instance (C a b) => C' a b

And now I can write:

C' Int

Which is of type:

C' Int :: * -> Constraint.

My question is, lets say I've got

type family T a b

i.e. of type:

 T :: * -> * -> *

Is there a way I can define T' such that I can write:

 T' Int

With type:

 T' :: * -> *

Much like I've done with the constraint type?

Clinton
  • 22,361
  • 15
  • 67
  • 163
  • I'm pretty sure GHC doesn't allow that with a type family, for [the reason it doesn't allow it with a type synonym](http://stackoverflow.com/questions/4922560/why-doesnt-typesynonyminstances-allow-partially-applied-type-synonyms-to-be-use). – David Young Mar 04 '17 at 04:15
  • It is possible if it's the type family ends in the type `Constraint` though with some with some class trickery as shown. I was just wondering whether I could extend that trickery to type families that don't end in the type `Constraint` – Clinton Mar 04 '17 at 04:17
  • One could use `type family T a :: * -> Constraint` but then instances can only depend on `a` e.g. `type instance T Int = K` where `K` is a one argument type class. – chi Mar 04 '17 at 07:33
  • The types of `C` and `T` are not `C :: * -> * -> Constraint` and `T :: * -> * -> *` - if they were, you wouldn't have this problem, as they would already be injective type constructors. The kinds of type families are currently inexpressible, but they are not function arrows. You can write `newtype T' a b = T' (T a b)` but it isn't really useful. – user2407038 Mar 04 '17 at 09:45
  • You want T to be an ordinary type contructor? Like `Either Int :: * -> *` – Euge Mar 04 '17 at 11:41
  • The [singletons](https://hackage.haskell.org/package/singletons) library may be relevant (or more generally, the [defunctionalization trick](https://typesandkinds.wordpress.com/2013/04/01/defunctionalization-for-the-win/) used therein). – kosmikus Mar 04 '17 at 13:57

0 Answers0