Repeated variables in type family instances
eir at cis.upenn.edu
Thu Jun 27 00:00:16 CEST 2013
Sure. Say you want a default type at any given kind. You could write something like this:
> type family Default (a :: k) :: k
> type instance Default (a :: *) = ()
> type instance Default (a :: * -> *) = 
> type instance Default (a :: * -> * -> *) = (,)
> type instance Default (a :: * -> * -> * -> *) = (,,)
This isn't perhaps the most useful example, but it works.
On Jun 26, 2013, at 8:33 AM, Dominique Devriese wrote:
> Thanks for your answers.
> 2013/6/24 Richard Eisenberg <eir at cis.upenn.edu>:
>> The nub of the difference is that type families can pattern-match on kinds,
>> whereas term-level functions cannot pattern-match on types. So, while the @a
>> is repeated in the pattern as written above, GHC does not, when matching a
>> pattern, check that these are the same. In fact, they have to be the same if
>> the function argument is well-typed. On the other hand, type family
>> equations *can* branch based solely on kind information, making the repeated
>> variable semantically important.
> Interesting, I wasn't aware this was possible. I agree that if it's
> possible to branch solely on kind info, then they should be taken into
> account for the linearity check. Do you perhaps have an example of how
> to do this sort of branching?
More information about the Glasgow-haskell-users