Let a function return different types depending on the values of the arguments

user_9418130 0
Viewed 80

Given this interface:

{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies   #-}
module Tlf where

import           Data.Dynamic  (Dynamic, fromDyn, toDyn)
import           Data.Kind     (Type)
import           Data.Proxy    (Proxy (Proxy))
import           Data.Typeable (Typeable)

data Q = Q1 | Q2
       deriving (Show)

data R1 = R1 deriving (Show)
data R2 = R2 deriving (Show)

newtype TL (a :: [Type]) = TL { unTL :: Dynamic }

someFun :: Q -> TL '[R1, R2]
someFun Q1 = (TL . toDyn) R1
someFun Q2 = (TL . toDyn) R2

I want to write a function that runs someFunc and extracts back the return value. This works:

myQ :: (Typeable a) => Proxy a -> Q -> a
myQ _ q = (fromDyn . unTL . someFun) q (error "This shouldn't happen!")

> myQ (Proxy :: Proxy R1) Q1
R1

But the additional Proxy is redundant and it is not as safe as it could be

*Tlf> myQ (Proxy :: Proxy R2) Q1
*** Exception: This shouldn't happen!

The thing is that I know that Q1 will yield R1. So I wrote this:

type family FunRes (a :: Q) :: Type where
  FunRes 'Q1 = R1
  FunRes 'Q2 = R2

But now I am stuck on how to put the pieces together. I tried:

myQ' :: forall q. q -> FunRes q
myQ' q = (fromDyn . unTL . someFun) q (error "This shouldn't happen!")

But ghc says no:

    • Expected kind ‘Q’, but ‘q’ has kind ‘*’
    • In the first argument of ‘FunRes’, namely ‘q’
      In the type signature: myQ' :: forall q. q -> FunRes q

I also tried a few other things, but I always stumble over the error given above.

haskell
1 Answers

The problem is, you're trying to make myQ return different types depending on the values of arguments (edit: when I wrote that, the question had a different title). This cannot happen. Haskell just doesn't support this sort of thing.

(if you want to look it up and research more, this is called "dependent types" - because the types depend on the values)

In Haskell, you can do certain half-measures. For example, a popular approach is called "singleton", where you make yourself a GADT of cases tagged with values of Q promoted to types:

data SQ (q :: Q) where
  SQ1 :: SQ Q1
  SQ2 :: SQ Q2

And then you make a function to convert from SQ to Q:

reflectQ :: SQ q -> Q
reflectQ SQ1 = Q1
reflectQ SQ2 = Q2

And then myQ can become:

myQ :: Typeable (FunRes q) => SQ q -> FunRes q
myQ q = (fromDyn . unTL . someFun) (reflectQ q) (error "This shouldn't happen!")

And you'd call it like this:

> myQ SQ1
R1

> myQ SQ2
R2

But this has one obvious gotcha: you can only pass SQ1 and SQ2 at compile time. They can't come from, say, user input.

Or, to be more precise, they can, but then you're back to not knowing the type of result. It will have to remain generic. Like I said at the top, Haskell ultimately doesn't support dependent types.

Also, if you squint hard enough, you can see that R1 and R2 already kind of play the role of SQ1 and SQ2, so you might as well just do this:

class RtoQ r where reflectRtoQ :: Q
instance RtoQ R1 where reflectRtoQ = Q1
instance RtoQ R2 where reflectRtoQ = Q2

myQ :: forall a. (Typeable a, RtoQ a) => a
myQ = (fromDyn . unTL . someFun) (reflectRtoQ @a) (error "This shouldn't happen!")

> myQ @R1
R1

> myQ @R2
R2

This is slightly worse than the "singleton" approach, because the values of SQ can be passed around, stored in data structures, and all the other things you can do with values, whereas types R1 and R2 cannot.

user_1802860
Related