Haskell Noob here.

An oversimplified case of what I'm trying to do here:

test :: Int -> a
test i = i -- Couldn't match expected type ‘a’ with actual type ‘Int’. ‘a’ is a rigid type variable bound by ...

I don't quite understand why this wouldn't work. I mean, Int is surely included in something of type a.

What I was really trying to achieve is this:

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

data EnumType = Enum1 | Enum2 | Enum3

data MyType (a :: EnumType) where
  Type1 :: Int -> MyType 'Enum1
  Type2 :: String -> MyType 'Enum2
  Type3 :: Bool -> MyType 'Enum3

myFunc :: EnumType -> MyType 'Enum1 -> MyType any
myFunc Enum1 t = t -- Can't match type `any` with `Enum1`. any is a rigid type variable bound by ...
myFunc Enum2 _ = Type2 "hi"
myFunc Enum3 _ = Type3 True

What is going on here? Is there a way to work around this or is it just something you can't do?

CodePudding user response：

For the GADT function you want to write, the standard technique is to use singletons. The problem is that values of type EnumType are value-level things, but you want to inform the type system of something. So you need a way to connect types of kind EnumType with values of type EnumType (which itself has kind Type). That's impossible, so we cheat: we connect types x of kind EnumType with values of a new type, SEnumType x, such that the value uniquely determines x. Here's how it looks:

data SEnumType a where
    SEnum1 :: SEnumType Enum1
    SEnum2 :: SEnumType Enum2
    SEnum3 :: SEnumType Enum3

myFunc :: SEnumType a -> MyType Enum1 -> MyType a
myFunc SEnum1 t = t
myFunc SEnum2 _ = Type2 "hi"
myFunc SEnum3 _ = Type3 True

Now the a in the return type MyType a isn't just fabricated out of thin air; it is constrained to be equal to the incoming a from SEnumType, and pattern matching on which SEnumType it is lets you observe whether a is Enum1, Enum2, or Enum3.

CodePudding user response：

Is there a way to work around this or is it just something you can't do?

I'm afraid that it's just "something you can't do". The reason is simple to explain.

When you write a type signature like (to take your first, simpler example)

test :: Int -> a

or, to write it the more literal, expanded form

test :: forall a. Int -> a

You are saying that literally, "for all a", this function can take an Int and return a value of type a. This is important, because calling code has to believe this type signature and therefore be able to do something like this (this isn't realistic code, but imagine a case where you feed the result of test 2 to a function that requires a Char or one of those other types):

test 2 :: Char
test 2 :: [Int]
test 2 :: (Double, [Char])

and so on. Clearly your function can't work with any of these examples - but it has to be able to work with any of them if you give it this type signature. Your code, quite simply, does not fit that type signature. (And nor could any, unless you "cheat" by having eg test x = undefined.)

This shouldn't be a problem though - the compiler is simply protecting you from a mistake, because I'm sure you realise that your code cannot satisfy this type signature. To take your "real" example:

myFunc :: EnumType -> MyType Enum1 -> MyType any

although this produces a compilation error, your code in the function is likely correct, and the problem is the type signature. If you replace it with

myFunc :: EnumType -> MyType Enum1 -> MyType Enum1

then it will compile (barring any further errors, which I've not checked it for), and presumably do what you want. It doesn't look like you actually want to be able to call myFunc and have it produce, say, a MyType Int. (If by any chance you do, I'd suggest you ask a separate question where you elaborate on what you actually need here.)

CodePudding user response：

As was already said, your signature expresses a universal type

myFunc :: ∀ a . EnumType -> MyType 'Enum1 -> MyType a

whereas what you're actually trying to express is an existential type

myFunc :: EnumType -> MyType 'Enum1 -> (∃ a . MyType a)

Haskell doesn't have a feature quite like that, but it does have some way to achieve essentially the same thing.

1. Both GADTs and the ExistentialTypes extension allow expressing existentials, but you need to define a separate type for them.

   data MyDynType where
     MyDynWrap :: MyType a -> MyDynType
   
   myFunc :: EnumType -> MyType 'Enum1 -> MyDynType
   myFunc Enum1 t = MyDynWrap t
   myFunc Enum2 _ = MyDynWrap $ Type2 "hi"
   myFunc Enum3 _ = MyDynWrap $ Type3 True
   

2. Maybe you don't even need a separate type, but can simply modify MyType to be “dynamic” in the first place.

   data MyType = Type1 Int | Type2 String | Type3 Bool
   
   myFunc :: EnumType -> MyType -> MyType
   myFunc Enum1 (Type1 i) = Type1 i
   myFunc Enum2 _ = Type2 "hi"
   myFunc Enum3 _ = Type3 True
   

3. existentials can be emulated at the spot, anonymously, by unwrapping a layer of continuation-passing style and then using the dual universal quantifier via the RankNTypes extension.

   {-# LANGUAGE RankNTypes #-}
   
   data MyType (a :: EnumType) where ... -- as original
   
   myFunc :: EnumType -> MyType 'Enum1 -> (∀ a . MyType a -> r) -> r
   myFunc Enum1 t q = q t
   myFunc Enum2 _ q = q (Type2 "hi")
   myFunc Enum3 _ q = q (Type3 True)