Source
r/haskellquestions•
tejon

MPTC+FunDep: get bare value of dependent type?

This fails with Could not deduce (Foo a0 b):

class Foo a b | a -> b where
  foo :: b

But this works fine:

class Bar a b | a -> b where
  bar :: Const b a

It seems like bar should carry no more actual data about a than foo, and all Const does is explicitly pull the instance variable into scope. But this fails the same as Foo:

type Const' a b = a
class Baz a b | a -> b where
  baz :: Const' b a

Meanwhile, this is fine:

class Qux a b | a -> b where
  qux :: a

What's really going on here? Is there any way I can get an unwrapped b?

Posted Aug 2, 2018, 9:08 PM UTC

33
CynicalHarry•

Well, think of it this way: a -> b means the type of b is determined by a, but if you use lets say foo :: Int it does not tell you anything about a and thus nothing about the value of foo.

An example of why this is important would be this:

class Foo a b | a -> b
  foo :: b

instance Foo Int Int where
  foo = 1
instance Foo String Int where
  foo = 2

If you now use a = foo :: Int is a then 1 or 2? You cannot know without knowing a. If your associated types are injective you can also add another b -> a fundep, which would make the second instance Foo String Int illegal.

To resolve your issue, you can use Const or if you like Tagged (from the tagged package) or you pass in a proxy or value.

class Foo a b | a -> b where
  foo :: Tagged a b

a = unTagged (foo :: Tagged Int Int) -- usage

-- or

class Foo a b | a -> b where
  foo :: Proxy a -> b
  foo :: proxy a -> b -- alternative definition

a = foo (Proxy :: Proxy Int)

-- or 

class Foo a b | a -> b where
  foo :: a -> b

a = foo (undefined :: Int)

The proxy approach is the cleaner version of the last one btw. I think there is also a way to do this with TypeApplications but I'm always confused as to how you supply the arguments for methods of type classes. You could try foo @a @b with a and b substituted for your concrete type.

PS: Its not called dependent type that term is reserved for a different thins entirely. Perhaps call is associated value.

2
tejonOP•

Ah... so basically, the answer is that Const requires the caller to know the type of a, while a type synonym does not. Makes sense!

If your associated types are injective you can also add another b -> a fundep

I was completely unaware that multiple fundeps were possible! They don't seem to pop up in examples anywhere. I guessed at the syntax and happily got it right on the first try (comma-separated), this is actually what I wanted in the first place!

PS: Its not called dependent type that term is reserved for a different thins entirely.

Isn't it a form of dependent pair, though? And it's a functional dependency. :)

1
CynicalHarry•

Nice to see you've found what you were looking for.

It is a functional dependency, but the 'dependent types' term is already taken. https://en.wikipedia.org/wiki/Dependent_type

1