CODEWITHSUNDEEP
haskell
Bryan Olivier
Bryan Olivier

Reputation: 5307

How can a functional type dependence be used to derive equality of type parameters?

Consider the following code:

{-# LANGUAGE RankNTypes, MultiParamTypeClasses, FunctionalDependencies #-}

data St t = St
    {       use_t :: t
    }

class S s t | s -> t
    where   -- Nothing really

newtype P s = P
    {       unP :: forall b t. (S s t) =>
                    St t
            ->      (St t -> b)     -- pok
            ->      b
    }

f :: (S s t) => t -> P s
f t = P $ \s pok -> pok s { use_t = t }

The code looks contrived, but the idea is that the class S is used to express that the type parameter t is determined by the type parameter s, so I don't have to add t as a type parameter to the type P.

The above code however in short gives the following error Could not deduce (t1 ~ t) from the context (S s t) or from (S s t1). This error message suggests that the compiler wants to use either one or the other of these contexts, whereas I would have hoped it would use both and conclude t1 ~ t from them.

I would appreciate any suggestions to get this working without adding t as a type parameter to type P.

Upvotes: 5

Views: 83

Answers (2)

Bryan Olivier
Bryan Olivier

Reputation: 5307

I ended up solving my problem differently, because I also had another problem with my approach that could not be solved this way. This other problem was the following:

{-# LANGUAGE RankNTypes, MultiParamTypeClasses, FunctionalDependencies #-}

data St t u = St
    {       use_u :: u
    ,       use_t :: t
    }

class Monad m => S s m t | s -> t

newtype P s u m a = P
    {       unP :: forall b t. {-(Monad m,S s m t) => -- Adding this causes problems with f -}
                    St t u
            ->      (a -> St t u -> m b)    -- pok
            ->      m b
    }

w :: a -> P s u m a
w x = P $ \s pok -> pok x s

f :: (S s m t) => P s u m ()
f = P $ \s pok -> unP (w ()) s pok

main = putStrLn "Hello world!"

Adding the type constraints in unP was essential for the other solution, but gave me trouble with this one. The t type parameter is only used in the St type, so I have now solved the problem there using GADTs. The solution to my original problem thus became:

{-# LANGUAGE RankNTypes, MultiParamTypeClasses, FunctionalDependencies, GADTs #-}
{-# LANGUAGE RecordWildCards #-}

data St s where
    St :: (S s t) =>
            {       use_t :: t
            } -> St s

class S s t | s -> t

newtype P s = P
    {       unP :: forall b.
                    St s
            ->      (St s -> b)     -- pok
            ->      b
    }

-- Apparently the record update syntax is not fully implemented for GADTs, especially when using polymorphic fields.
-- See https://www.reddit.com/r/haskell/comments/3r30pp/updating_polymorphic_records/?st=j5sno89f&sh=4ad675fb
-- If you write your own update functions, trouble can be alleviated a bit using RecordWildCards .
f :: (S s t) => t -> P s
-- f t = P $ \s pok -> pok s { use_t = t }
f t = P $ \s pok -> pok $ update_use_t t s
    where
    update_use_t t = \(St {..}) -> St {use_t = t, ..}

main = putStrLn "Hello world!"

The solution to my second problem thus became:

{-# LANGUAGE RankNTypes, MultiParamTypeClasses, FunctionalDependencies, GADTs #-}
data St s u where
    St :: (Monad  m,S s m t) =>
            {       use_u :: u
            ,       use_t :: t
            } -> St s u

class Monad m => S s m t | s -> t

newtype P s u m a = P
    {       unP :: forall b.
                    St s u
            ->      (a -> St s u -> m b)    -- pok
            ->      m b 
    }

w :: a -> P s u m a
w x = P $ \s pok -> pok x s

f :: (S s m t) => P s u m ()
f = P $ \s pok -> unP (w ()) s pok

main = putStrLn "Hello world!"

This solution may eventually still benefit from the type equivalence constraints as suggested by dfeuer.

Upvotes: 0

dfeuer
dfeuer

Reputation: 48591

You can't do it with the class as written. See Can I magic up type equality from a functional dependency?. But you can do it with a different class:

class t ~ T s => S s t where
  type T s :: *

You'll need to define T for each instance, but at least that's not hard. And you can provide a default definition of T if there's an appropriate one.

Upvotes: 3

Related Questions