2

Let's say I have the following:

type family TF a b

Can I write something like this

type instance TF Int t = (t ~ (x,y)) => (Int,x,y)

as a perhaps silly example.

This question is along the same theme as the accepted answer to this question: Haskell: Equality constraint in instance

I want to match the type instance even if I'm not sure the second argument is a pair then force the second argument to be a pair (with a resulting compile error if this is not successful).

Community
  • 1
  • 1
Clinton
  • 22,361
  • 15
  • 67
  • 163
  • I'd guess not, since `x,y` are not in scope. As written, that would essentially involve existential types, which are not "first-class" in Haskell. – chi Feb 15 '16 at 16:37
  • 1
    `type family Fst x where Fst (x,y) = x; type family Snd x where Snd (x,y) = y; type instance TF Int t = (Int, Fst t, Snd t)`. The simpler thing to do is to give your index a single, closed family which only reduces for pairs: `type instance TF Int x = TF_Int x; type family TF_Int x where TF_Int (x,y) = (Int, x, y)`. – user2407038 Feb 15 '16 at 17:01
  • @user2407038, I believe the `Fst`/`Snd` approach is "lazier", and will therefore allow more useful reductions. – dfeuer Feb 15 '16 at 21:11

1 Answers1

4

You might be able to do this in GHC 8.0 using the new TypeError feature, depending on what you mean by "force the second argument to be a pair". 

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances #-}

module Pair where

import GHC.TypeLits

type family Fst p where
  Fst (x, y) = x
  Fst _t = TypeError (Text "Fst: expected a pair, but got " :<>: ShowType _t)

type family Snd p where
  Snd (x, y) = y
  Snd _t = TypeError (Text "Snd: expected a pair, but got " :<>: ShowType _t)

type family TF a b
type instance TF Int t = (Int, Fst t, Snd t)

Now you should get a compile error if you try to apply TF Int to a non-tuple:

*Pair> let x = x in x :: TF Int Bool

<interactive>:9:1: error:
    • Fst: expected a pair, but got Bool
    • When checking the inferred type
        it :: (Int, (TypeError ...), (TypeError ...))

However, this doesn't really "force" the argument to be a pair any more than calling fromJust "forces" its argument to be of the form Just x. It is really programming with partial functions at the type level.

Well-formedness of type family applications is totally determined by the kind of the type family, and a pair (x, y) has the same kind * as, say, Bool does. You can't magically incur a constraint simply by writing down an application of a type family. If you want to get a constraint at the type level, you have to write it to the left side of =>.

In the linked question, CanFilter (b -> c) a is already a constraint, so it can imply b ~ c.

Reid Barton
  • 14,951
  • 3
  • 39
  • 49
  • "It is really programming with partial functions at the type level." I don't think this is exactly true here - it would be more true without the `TypeError` case. In that case, you get `TF Int Bool ~ (Int, Fst Bool, Snd Bool)` - the last two types are "stuck" (i.e. they can *never* be reduced) but they do not produce a type error. But `Fst Bool` is still inhabited by bottom! The point of `TypeError` is so if it *ever* appears in a type, it is really a type error. `Fst Bool` *with* the TypeError is *not* inhabited by bottom - because the type itself simply does not exist. – user2407038 Feb 16 '16 at 05:01
  • I don't follow. If I don't have a `TypeError` case, then `Fst` is total; `Fst Int` is a stuck type like you say. The purpose of `TypeError` is to make `Fst Int` an error, so `Fst` becomes partial. – Reid Barton Feb 16 '16 at 14:51