Use declared variable in instance definition in Haskell

Question

I'm trying to implement (a simplified version of) Representable for my data type, but I'm not allowed to use the first data type parameter in the definition:

question.hs
-----------

{-# LANGUAGE TypeFamilies #-}

class Representable f where
   type Rep f :: *
   tabulate :: (Rep f -> x) -> f x
   index    :: f x -> Rep f -> x

data F a b = F a b

instance Representable (F a) where
--                        ^
-- orfeas: It's right here, ghc!
  type Rep (F a) = a
  tabulate g = F a (g a)
  --             ^    ^
  -- ghc:        a not in scope :(
  index (F a b) = g where g a = b

main = return ()

How can I make ghc see a inside the instance implementation?

I expected the above to compile successfully, but I got this instead:

ghc -dynamic question.hs
[1 of 1] Compiling Main             ( question.hs, question.o )

question.hs:15:18: error: Variable not in scope: a
   |
14 |   tabulate g = F a (g a)
   |                  ^

question.hs:15:23: error: Variable not in scope: a
   |
14 |   tabulate g = F a (g a)
   |                       ^

I see the answer already alluded to it, but I'm not sure you've followed, so: in tabulate g = F a (g a), F takes values, not types, and a is a type. — Louis Wasserman
– Louis Wasserman, Commented Dec 10, 2022 at 23:03

leftaroundabout · Accepted Answer · 2022-12-10 20:35:25Z

2

a is a type-level variable, but you're trying to use it in a value-level equation.

Let's call the type- and value-level constructors differently to make it clearer:

data FTL a b = FVL a b

Even clearer (but still the same thing) with annotations:

{-# LANGUAGE GADTSyntax, KindSignatures #-}

data FTL :: Type -> Type -> Type where
  FVL :: a -> b -> FTL a b

Let's also add some annotations in your proposed instance:

{-# LANGUAGE InstanceSigs, UnicodeSyntax, ScopedTypeVariables #-}

instance ∀ (a :: Type) . Representable (FTL a) where
  type Rep (FTL a) = a
  tabulate :: (a -> x) -> F a x
  tabulate g = FVL (a :: Type??)
                   (g (a :: Type??) :: x)

It doesn't make sense to give something of type Type to a value-level constructor, nor to the function g. Instead, you should give a value of type a to them. But, well – you can't actually do that here, because you have no such value.

Really, the problem is that F a is not a representable functor.

answered Dec 10, 2022 at 20:35

leftaroundabout

121k6 gold badges185 silver badges337 bronze badges

Sign up to request clarification or add additional context in comments.

3 Comments

orfeas Over a year ago

Thanks! I think that there should be a way to make this representable though, as it's demanded (in a roundabout way) by ex. 6 of bartoszmilewski.com/2016/04/18/adjunctions.

leftaroundabout Over a year ago

@orfeas pretty sure you're interpreting something wrong there, but this seems to be a good topic to ask another question about.

chi Over a year ago

@orfeas AFAICS, in ex. 6 the product is a left adjoint, the function is the right one. You should able to let data F a b = F (a->b) (the right adjoint) and define instance Representable (F a).

Collectives™ on Stack Overflow

Use declared variable in instance definition in Haskell

1 Answer 1

3 Comments

Your Answer

Hot Network Questions

Collectives™ on Stack Overflow

1 Answer 1

3 Comments

Your Answer

Sign up or log in

Post as a guest

Related