DataKind Unions

  • A+
Category:Languages

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?

 


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).

Comment

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen: