How do you get and use a dependent type from a type class with functional dependencies?

Question

How do you get and use a dependent type from a type class with functional dependencies?

To clarify and give an example of my last attempt (minimized from the actual code that I wrote):

class Identifiable ab | a -> b where -- if you know a, you know b idOf :: a -> b instance Identifiable Int Int where idOf a = a f :: Identifiable Int b => Int -> [b] -- Does ghc infer b from the functional dependency used in Identifiable, and the instance? fa = [5 :: Int] 

But ghc does not output b, it seems as it prints this error:

 Couldn't match expected type 'b' with actual type 'Int' 'b' is a rigid type variable bound by the type signature for f :: Identifiable Int b => Int -> [b] at src/main.hs:57:6 Relevant bindings include f :: Int -> [b] (bound at src/main.hs:58:1) In the expression: 5 :: Int In the expression: [5 :: Int] In an equation for 'f': fa = [5 :: Int] 

For context, here is a less minimal example:

 data Graph a where Graph :: (Identifiable ab) => GraphImpl b -> Graph a getImpl :: Identifiable ab => Graph a -> GraphImpl b getImpl (Graph impl) = impl 

The workaround here is to add b as type arg to Graph:

 data Graph ab | a -> b where Graph :: (Identifiable ab) => GraphImpl b -> Graph a 

Full context: I have Graph objects, each of which has an identifier, each object is assigned a value of 1 node. You can find the node object by object. I also have a Graph' , which consists of nodes (which entities can be assigned to), and to search for a node you need to provide the identifier node, which is Int. Graph uses Graph' internally. I have an IdMap that maps object identifiers to node identifiers in Graph' . This is my definition of Graph :

 data Graph a where Graph :: (Identifiable ab) => { _idMap :: IdMap b, _nextVertexId :: Int, _graph :: Graph' a } -> Graph a 

---

Answer : use family types, see Daniel Wagner's answer . For a full story, see Reid Burton's Answer .

Answer 1

It seems a little strange that the GHC complains about the minimum f that you placed at the very top. But this seems to work with type families:

 {-# LANGUAGE TypeFamilies #-} class Identifiable a where type IdOf a idOf :: a -> IdOf a instance Identifiable Int where type IdOf Int = Int idOf a = a f :: a -> [IdOf Int] f _ = [5 :: Int] 

Perhaps you can adapt this idea to your larger example.

Answer 2

In a GHC implementation, functional dependencies may limit the values ​​of type variables that would otherwise be ambiguous (in the sense of show . read ). They cannot be used to provide evidence that the two types are equal, thus, what the limitations of equality may be. My understanding is that functional dependencies precede the addition of coercions to the intermediate main GHC language, and these coercions are necessary in general to translate those programs that you expect to work in well-typed main programs.

(This situation may be best, since the GHC does not actually apply the condition of functional dependency at the global level, and it would be easy to violate type safety if programs like your first were adopted. On the other hand, the GHC could also the best job of ensuring global instance consistency.)

A short version of this is that the type checking logic around functional dependencies is not as strong as you might expect, especially in combination with newer types of system functions such as GADT. Instead, I recommend using type families in these situations, as shown in Daniel Wagner's answer.

https://ghc.haskell.org/trac/ghc/ticket/345 is an old ticket on a similar topic, so you can see that this is a long-standing known issue with functional dependencies and using type families instead is an officially recommended solution.

If you want to maintain a style in which Identifiable has two type arguments, you can also customize your program in the form

 type family IdOf a class (b ~ IdOf a) => Identifiable ab where idOf :: a -> b type instance IdOf Int = Int instance Identifiable Int Int where idOf a = a f :: Identifiable Int b => Int -> [b] fa = [5 :: Int]