DataKind Unions

Question

I'm not sure if it is the right terminology, but is it possible to declare function types that take in an 'union' of datakinds?

For example, I know I can do the following:

{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE GADTs          #-}

...

data Shape'
  = Circle'
  | Square'
  | Triangle'

data Shape :: Shape' -> * where
  Circle :: { radius :: Int} -> Shape Circle'
  Square :: { side :: Int} -> Shape Square'
  Triangle
    :: { a :: Int
       , b :: Int
       , c :: Int}
    -> Shape Triangle'

test1 :: Shape Circle' -> Int
test1 = undefined

However, what if I want to take in a shape that is either a circle or a square? What if I also want to take in all shapes for a separate function?

Is there a way for me to either define a set of Shape' kinds to use, or a way for me to allow multiple datakind definitions per data?

Edit:

The usage of unions doesn't seem to work:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds       #-}
{-# LANGUAGE GADTs           #-}
{-# LANGUAGE KindSignatures  #-}
{-# LANGUAGE PolyKinds       #-}
{-# LANGUAGE TypeFamilies    #-}
{-# LANGUAGE TypeOperators   #-}

...

type family Union (a :: [k]) (r :: k) :: Constraint where
  Union (x ': xs) x = ()
  Union (x ': xs) y = Union xs y

data Shape'
  = Circle'
  | Square'
  | Triangle'

data Shape :: Shape' -> * where
  Circle :: { radius :: Int} -> Shape Circle'
  Square :: { side :: Int} -> Shape Square'
  Triangle
    :: { a :: Int
       , b :: Int
       , c :: Int}
    -> Shape Triangle'

test1 :: Union [Circle', Triangle'] s => Shape s -> Int
test1 Circle {} = undefined
test1 Triangle {} = undefined
test1 Square {} = undefined

The part above compiles

Watchman

Answer 1

You can accomplish something like this in (I think) a reasonably clean way using a type family together with ConstraintKinds and PolyKinds:

type family Union (a :: [k]) (r :: k) :: Constraint where
  Union (x ': xs) x = ()
  Union (x ': xs) y = Union xs y

test1 :: Union [Circle', Triangle'] s => Shape s -> Int
test1 = undefined

The () above is the empty constraint (it's like an empty "list" of type class constraints).

The first "equation" of the type family makes use of the nonlinear pattern matching available in type families (it uses x twice on the left hand side). The type family also makes use of the fact that if none of the cases match, it will not give you a valid constraint.

You should also be able to use a type-level Boolean instead of ConstraintKinds. That would be a bit more cumbersome and I think it would be best to avoid using a type-level Boolean here (if you can).

Side-note (I can never remember this and I had to look it up for this answer): You get Constraint in-scope by importing it from GHC.Exts.

Edit: Partially disallowing unreachable definitions

Here is a modification to get it to (partially) disallow unreachable definitions as well as invalid calls. It is slightly more roundabout, but it seems to work.

Modify Union to give a * instead of a constraint, like this:

type family Union (a :: [k]) (r :: k) :: * where
  Union (x ': xs) x = ()
  Union (x ': xs) y = Union xs y

It doesn't matter too much what the type is, as long as it has an inhabitant you can pattern match on, so I give back the () type (the unit type).

This is how you would use it:

test1 :: Shape s -> Union [Circle', Triangle'] s -> Int
test1 Circle {}   () = undefined
test1 Triangle {} () = undefined
-- test1 Square {} () = undefined -- This line won't compile

If you forget to match on it (like, if you put a variable name like x instead of matching on the () constructor), it is possible that an unreachable case can be defined. It will still give a type error at the call-site when you actually try to reach that case, though (so, even if you don't match on the Union argument, the call test1 (Square undefined) () will not type check).

Note that it seems the Union argument must come after the Shape argument in order for this to work (fully as described, anyway).

Greg

Cool technique! I didn't know you could do nonlinear matching in type families like this. – Godard

Though, isn't x ~ x redundant because we're already in the nonlinear pattern for x? Seems like () should work just as well. – Godard

@Godard I would think so too, but if you use () instead of x ~ x for some reason it no longer prevents you from putting unreachable pattern matches in your function. Also, you must have an explicit type annotation inside your pattern match for that “unreachable” check to happen (with x ~ x). I’m also not sure why that’s the case (maybe a GHC bug?). – Greg

To clarify a bit: By "explicit type annotation inside your pattern match," I mean something like: test2 (Square s :: Shape Square') = .... And, like I said, I'm not sure why that is needed here (and, to me, it almost seems like it could be the result of some sort of GHC bug). – Greg

that does sound like a GHC bug to me, at least on the surface (there might be deep subtlety here). In the unreachable case, shouldn't the type family fail to normalize? Worth reporting I think, see what the gurus say. – Godard

@Godard Based on my previous experience with type families I would think so, yeah. I would think it would fail to normalize regardless of strange x ~ x things or explicit type annotations in patterns. Maybe it is worth reporting just in case (and even if it isn't a bug, I can probably get a good explanation of why it works the way it does!). – Greg

Oh, I just realized I had an older version of GHC (8.4.3). If I upgrade to the latest (8.6.3), then the x ~ x no longer matters (it can be replaced with ()), but for some reason the explicit type annotations are still necessary. – Greg

Thank you! I will try this later and accept the answer if it works. Do you mind adding back the x ~ x as a note for those who are using older versions? – Watchman

@AllanW Looking at this again, it looks like I was mistaken about a couple of things: The explicit type annotation seems to give errors regardless of whether the pattern match is type-correct (not fully sure why, could be a limitation of GADT pattern matching). It looks like I was misinterpreting the type error messages. Also, it looks like there is not in fact a difference between GHC versions. I'm not sure what made me think there was a difference with x ~ x now, because I can't seem to reproduce it. Sorry for the confusion! – Greg

It will still work for preventing invalid calls, but it won't seem to prevent unreachable cases in a function definition. That might be possible, but I am not sure how (so far, at least). – Greg

Can you take a look at my edit? Using your example, passing a square still compiles. I'm not sure if this relates to your 'explicit type annotation' comment above – Watchman

@AllanW This is what I meant when I was saying it won't prevent unreachable cases to be defined. If you actually try to call that function with a Shape Square', it will not type check (but cases that should type check, do type check). For example, the call test1 (Square undefined) gives you a type error while test1 (Circle undefined) does not. There may be a way to also prevent the unreachable code in definitions by extending this technique, but I'm not sure (so far). – Greg

@AllanW I edited in a partial solution to the unreachable case issue. – Greg

@David I've accepted your answer, but I'm curious how the first example with Constraint is meant to be used? I'm not very familiar with anything related to DataKinds beyond the basic example. – Watchman

@AllanW You would use the first example by putting a constraint of this form in your type: Union [...] t => {rest of your type goes here} where [...] is a list of the types you want to restrict t to (where t is the name of the type variable you are restricting. Here, this is s). Does that make sense? Let me know if you want more clarification. – Greg

Note that this will might not work out too well for the kind * (the kind that consists of the "usual" types). It should really just work for any kind you have defined yourself (or defined by a library), such as your Shape' kind here. I haven't tested * out though. It may still work if you are dealing with a GADT, but I am not sure. So if you are not using a GADT at all and you are trying to use it with kind *, you may run into issues (although, you probably shouldn't be doing that anyway, hah). – Greg

@David it's been a while, but I'm wondering if there is a good way to use Union to restrict against pattern matching. For instance, if I have a data structure where the Shape field must be a square or triangle, the compiler will still complain that matching against those two alone is not exhaustive – Watchman

For reference, I ended up making a new question for pattern matching restrictions: #55556560 – Watchman

Answer 2

This is getting kind of awful, but I guess you could require a proof that it's either a circle or a square using Data.Type.Equality:

test1 :: Either (s :~: Circle') (s :~: Square') -> Shape s -> Int

Now the user has to give an extra argument (a "proof term") saying which one it is.

In fact you can use the proof term idea to "complete" bradm's solution, with:

class MyOpClass sh where
    myOp :: Shape sh -> Int
    shapeConstraint :: Either (sh :~: Circle') (sh :~: Square')

Now nobody can go adding any more instances (unless they use undefined, which would be impolite).

Godard

At this point, wouldn't this be the same as creating another data class whose constructors allow for a subset of shapes? The benefit I guess is that the function type still takes in Shape. To repeat the comment I added in the other post, I'm mainly using this to limit inputs for other data types (eg one type can only take in a circle or a triangle). My haskell experience is limited, but is there a way of specifying that constraint using typeclasses? – Watchman

@AllanW Yes you can use a class in a GADT, for example. data Scene where BasicShape :: MyOpClass s => Shape sh -> Scene. – Godard

@Godard Using a typeclass doesn't seem like the right solution for a GADT. I would prefer 'collapsing' the indirection by defining data Scene where BasicShape :: Either (s :~: Circle') (s :~: Square') -> Shape sh -> Scene, so providing the witness directly. – Meeting

@bradm, yeah, I probably agree. This whole problem seems like a bunch of hoop-jumping, honestly. I would be looking for an alternative design... – Godard

Why not Either (Shape Circle') (Shape Square') -> Int? – Anasarca

@DanielWagner, derp, yeah. Hoop jumping indeed. – Godard

@DanielWagner I can't believe I didn't see that. That would be much simpler. – Meeting

Answer 3

You could use typeclasses:

class MyOpClass sh where
    myOp :: Shape sh -> Int

instance MyOpClass Circle' where
    myOp (Circle r) = _

instance MyOpClass Square' where
    myOP (Square s) = _

This doesn't feel like a particularly 'complete' solution to me - anyone could go back and add another instance MyOpClass Triangle' - but I can't think of any other solution. Potentially you could avoid this problem simply by not exporting the typeclass however.

Meeting

My problem stems mainly from defining other data types. For instance, say I have a new data class who's constructor takes in either a circle or a square. How do I specify that using the typeclass? – Watchman

I don't quite understand what you mean by that. Do you mean you want to define a data type which can have a Shape Circle' or Shape Square' field, but not a Shape Triangle'? – Meeting

Oh, just saw your comment on @luqui's answer explaining it. Never mind. – Meeting

Answer 4

Another solution I've noticed, though pretty verbose, is to create a kind that has a list of feature booleans. You can then pattern match on the features when restricting the type:

-- [circleOrSquare] [triangleOrSquare]
data Shape' =
  Shape'' Bool
          Bool

data Shape :: Shape' -> * where
  Circle :: { radius :: Int} -> Shape (Shape'' True False)
  Square :: { side :: Int} -> Shape (Shape'' True True)
  Triangle
    :: { a :: Int
       , b :: Int
       , c :: Int}
    -> Shape (Shape'' False True)

test1 :: Shape (Shape'' True x) -> Int
test1 Circle {}   = 2
test1 Square {}   = 2
test1 Triangle {} = 2

Here, Triangle will fail to match:

    • Couldn't match type ‘'True’ with ‘'False’
      Inaccessible code in
        a pattern with constructor:
          Triangle :: Int -> Int -> Int -> Shape ('Shape'' 'False 'True),
        in an equation for ‘test1’
    • In the pattern: Triangle {}
      In an equation for ‘test1’: test1 Triangle {} = 2
   |
52 | test1 Triangle {} = 2
   |       ^^^^^^^^^^^

Unfortunately, I don't think you can write this as a record, which may be clearer and avoids the ordering of the features.

This might be usable in conjunction with the class examples for readability.

Watchman