Generic types with Type.Reflection and Nats

Question

I have a simple definition for a Nat and a definition for types indexed by Nat's, Natty.

data Nat :: * where 
    Zero :: Nat
    Suc  :: Nat -> Nat              deriving(Show, Typeable)

data Natty :: Nat -> * where
    Zy :: Natty Zero
    Sy :: Natty n -> Natty (Suc n)  deriving Typeable

I want to store and manipulate these Natty's in a generic fashion with the use of the Type.Reflection module.

Storing as a Nat as a type rep works fine.

foo :: Nat -> SomeTypeRep
foo x = SomeTypeRep (typeOf x)

But storing a Natty as a type rep doesn't work unless extra constraints are added.

boo :: Natty n -> SomeTypeRep
boo x = SomeTypeRep (typeOf x)

boo produces the following error:

No instance for (Typeable n) arising from the use of 'typeOf'

My question is why can Haskell not recognise that n is a nat and should therefore be Typeable?

Like I said I can fix this issue by adding the constraint of Typeable n to the beginning of boo but when I'm using a function that returns natty in the middle of another function its not that simple.

The following extensions and imports have been used.

{-# LANGUAGE DataKinds, KindSignatures, GADTs #-} 
import Type.Reflection

Alec · Accepted Answer · 2018-02-15 17:19:52Z

Adding Typeable n reflects the fact that GHC will need to pass in a different Typeable dictionary into boo if it is called with n instantiated differently.

There is some cleverness around the interplay of Typeable and DataKinds. The instances that GHC derives are roughly equivalent to

instance Typeable Nat where ...
instance Typeable 'Zero where ...
instance Typeable n => Typeable ('Suc n) where ...

The Typeable n constraint you are being prompted to add in will not be filled in by the Typeable Nat instance (remember n has kind Nat, not *!), but by the latter two constraints.

But, I can hear you saying, why can't GHC figure out by simple induction on those two instances that all n :: Nat are Typeable? Because 'Zero and 'Suc are not the only way of making something of kind Nat...

ghci> type family Stuck :: k
ghci> :kind Natty Stuck          -- a valid type!
Natty Stuck :: *

In other words, GHC can't know at compile time that n :: Nat is Typeable, you need to pass it a runtime witness of this fact.

Yes, but with a Natty, you actually have all the evidence you need. See my answer.
@dfeuer Interesting! You still end up having to traverse the whole Natty at runtime, but the problem is sliced differently. The App pattern looks new - I haven't seen it before.
it came in with Type.Reflection in GHC 8.2. The whole Typeable situation is much less unsatisfactory now.

dfeuer · Accepted Answer · 2018-02-16 05:26:11Z

You can implement the function you want, but not for free.

boof :: Natty n -> TypeRep n
boof Zy = typeRep
boof (Sy n) = withTypeable (boof n) typeRep

More explicitly (this is basically what happens under the hood in boof):

goo :: Natty n -> TypeRep n
goo Zy = typeRep @'Zero
goo (Sy n) = App (typeRep @'Suc) (goo n)

As goo shows, the structure of the TypeRep is actually very similar to the structure of the Natty. Indeed, you can go the other way too, although you can't convince the pattern checker that it's total:

hum :: TypeRep n -> Natty n
hum (App s n)
  | Just HRefl <- eqTypeRep s (typeRep @'S) = Sy (hum n)
  | otherwise = error "imp possible"
hum z
  | Just HRefl <- eqTypeRep z (typeRep @'Z) = Zy
  | otherwise = error "impposs ible"

You can wrap up the result as you wish:

boo :: Natty n -> SomeTypeRep
boo n = SomeTypeRep (boof n)

But it seems likely that you should use something a bit more specific than SomeTypeRep. The Typeable internals actually use this:

data SomeKindedTypeRep k where
  SomeKindedTypeRep :: forall (x :: k). Typeable x => SomeKindedTypeRep k

You can define that and use SomeKindedTypeRep Nat, or define a specialized version just for Nat. That way you don't lose track of the kind (known at compile time) just because you're intentionally forgetting the type.

Collectives™ on Stack Overflow

Generic types with Type.Reflection and Nats

2 Answers 2

3 Comments

Comments

Hot Network Questions

Collectives™ on Stack Overflow

2 Answers 2

3 Comments

Comments

Related