Eliminators and Typeclasses

[LeanderK]

I am wondering whether Eliminators can help prove that this is valid:

I have a normal HList:

data HList (ts :: [Type]) where
    HNil :: HList '[]
    (:&:) :: t -> HList ts -> HList (t ': ts)

infixr 5 :&:

instance (Show (HList '[])) where
    show _ = "[]"

instance (Show a, Show (HList ts)) => (Show (HList (a : ts))) where
    show (a :&: rest) = show a ++ ":&:" ++ show rest

and a homogenous case

newtype HoHeList (n :: Nat) a = HoHeList
    { unHoHeList :: HList (Replicate n a)
    }

now, i want to create a show-instance:

instance Show a => Show (HoHeList (n :: Nat) a) where
    show = (show . unHoHeList)

and prove it via (i am using your cong):

type TypeClassInduction a (n :: Nat) (f :: [Type] -> Type) (t :: Type -> Constraint)
    = t (f (Replicate n a))
$(genDefunSymbols [''TypeClassInduction])

typeClassInduction :: forall (n :: Nat) (a :: Type) (f :: [Type] -> Type) (t :: Type -> Constraint). 
    (SingI n, t (f '[a]), forall xs x. (t (f xs), t x) => t (f (x ': xs))) 
    => TypeClassInduction a n f t
typeClassInduction = elimNat @(TypeClassInduction a n f t) @n (sing @Nat @n) base step
        where
            base :: TypeClassInduction a 0 f t
            base = Refl
    
            step :: forall (k :: Nat).
                Sing k 
                -> TypeClassInduction a k f t
                -> TypeClassInduction a (k :+ 1) f t
            step _ = case replicateSucc @k @a of
                        Refl -> cong @_ @_ @((:$$) (what should i pass here...i don't really understand :$$))

it seems like I could just use elimNat again, but I am not sure. I get these errors that I am not sure how to solve:

$(genDefunSymbols [''TypeClassInduction])

results in

Expected kind ‘* -> Constraint’, but ‘t0’ has kind ‘* -> *’

removing it results genDefunSymbols in

Expected a type, but
      ‘TypeClassInduction a n f t’ has kind
      ‘Constraint’

This is understandable since I am not returning a type, but instead a constraint. Is there a way to solve this?

(also, forall xs x. (t (f xs), t x) => t (f (x ': xs)) is not valid haskell...but it seemed natural to write)

Edit:
replicateSucc is defined as

axiom :: a :~: b
axiom = unsafeCoerce Refl

replicateSucc :: forall k a. Replicate (k :+ 1) a :~: (a : Replicate k a)
replicateSucc = axiom

[LeanderK]

Also, I have just played a bit around with your eliminators package a few months ago, but writing this was easy. I this would not be some constraint, but instead a normal type, I think I would have figured it out myself! 🙂

[RyanGlScott]

Urk. I believe this is a GHC bug—in particular, Trac #11715—rearing its ugly head. In GHC Core, the Constraint and Type kinds are actually the same, which unfortunately means that there are certain places where GHC will confuse the two, such as Template Haskell reification. As a consequence, genDefunSymbols will produce ill-kinded types, since the information it reified was itself ill-kinded.

I'm afraid the only workaround for the time being is to just create the defunctionalization symbols by hand:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Foo where

import Data.Kind
import Data.Singletons
import Data.Singletons.Prelude.List
import GHC.TypeNats

type TypeClassInduction a (n :: Nat) (f :: [Type] -> Type) (t :: Type -> Constraint)
    = t (f (Replicate n a))
data TypeClassInductionSym0 :: k ~> Nat ~> ([Type] -> Type) ~> (Type -> Constraint) ~> Constraint
data TypeClassInductionSym1 :: k -> Nat ~> ([Type] -> Type) ~> (Type -> Constraint) ~> Constraint
data TypeClassInductionSym2 :: k -> Nat -> ([Type] -> Type) ~> (Type -> Constraint) ~> Constraint
data TypeClassInductionSym3 :: k -> Nat -> ([Type] -> Type) -> (Type -> Constraint) ~> Constraint
type instance Apply  TypeClassInductionSym0 a          = TypeClassInductionSym1 a
type instance Apply (TypeClassInductionSym1 a) n       = TypeClassInductionSym2 a n
type instance Apply (TypeClassInductionSym2 a  n) f    = TypeClassInductionSym3 a n f
type instance Apply (TypeClassInductionSym3 a  n  f) t = TypeClassInduction     a n f t

[LeanderK]

okay, thank you!
But I am still not sure how I can do a induction over some constraint.
I can't return TypeClassInduction a n f t....or can I (i am not really sure what's possible and what's not 😉)?

[RyanGlScott]

I'm not sure either!

All of the code in this library is built around predicates p such that p :: <datatype> ~> Type. You're trying to use an exotic predicate of kind <datatype> ~> Constraint, which certainly won't kind-check with the eliminators in this library. Moreover, I don't how one would even write a hypothetical eliminator that would support such a predicate. It's certainly not something I've ever seen in any dependently typed languages—are there examples out there of folks doing this sort of thing?

[LeanderK]

I don't know either 😀 This was more out of need (all this hassle leads me trying to write a good old Show-Instance).

I, unfortunately, have not much experience with "other" dependently typed languages, I have just played around with idris a bit and that's all.

[RyanGlScott]

In any case, you're barking up the wrong tree with typeClassInduction—it's not going to be well kinded either, as its return type is of kind Constraint, not Type, so it's not even a well formed function.

I suspect what you really want is something akin to a type-level eliminator. Something like:

type family ElimNatC (p :: Nat ~> Constraint) (s :: Nat) (pZ :: p @@ Z) (pS :: forall (n :: Nat). p @@ n -> p @@ (S n)) :: p @@ s where ...

Sadly, this is not possible in today's GHC, as its support for higher-ranked kinds in type families is extremely limited (see Trac #11719).

[LeanderK]

yeah, I knew that this is not a well-defined function, I hoped there is something like :~: for general constraints.
Hmm, so what can I do now? Any Idea? I don't think unsafeCoerce will work...

[RyanGlScott]

Hmm, so what can i do now?

Not much, I'm afraid. You're sailing through relatively uncharted waters on the fringes of GHC's type system, and you shouldn't be surprised if you hit impasses like this. There may be some other way to define your Show instance, but one thing is clear: eliminators aren't the solution (at present).

[LeanderK]

Thank you for your patience 🙂
It's not only uncharted, I am also (not yet?) that knowledgable what my GHC is capable of and what's impossible.

[LeanderK]

I don't want to bother you, but...could a different formulation of eliminators maybe work when i try something like like this?
(bogus, but my "inspiration")

type CanShow a n = HList (Replicate n a) -> String
$(genDefunSymbols [''CanShow])

canShowInduction :: forall (n :: Nat) (a :: Type) y (as :: [Type]). 
        (SingI n, Show a) 
    => CanShow a n
canShowInduction = elimNat @(CanShowSym1 a) @n (sing @Nat @n) base step
    where
        base :: CanShow a 0
        base = show

        step :: forall (k :: Nat).
            Sing k 
            -> CanShow a k
            -> CanShow a (k :+ 1)
        step _ _ = case replicateSucc @k @a of
                    Refl -> show

with a different formulation of step, so maybe something like this:

type ShowConstraint a n = Show (HList(Replicate n a))
type CanShow a n = HList (Replicate n a) -> String
$(genDefunSymbols [''CanShow])

canShowInduction :: forall (n :: Nat) (a :: Type) y. 
        (SingI n, Show a) 
    => CanShow a n
canShowInduction = elimNat @(CanShowSym1 a) @n (sing @Nat @n) base step
    where
        -- (how can i get the (ShowConstraint a 0) from here?)
        base :: CanShow a 0
        base = show

        step :: forall (k :: Nat). (ShowConstraint a k)
           --- (ShowConstraint a k = Show(HList(Replicate a k))
            Sing k 
            -> CanShow a (k :+ 1)
        step _ = case replicateSucc @k @a of
                    -- (so we have (Replicate a (k + 1) ~ (a : Replicate a (k)))
                    Refl -> show

I don't know whether this would actually help or just move the problem into eliminators.
Also, I don't know whether GHC could figure it out, but I would guess so since show then exactly has the information it needs.
Another minor Problem here is that I can't replace it with an unsafeCoerce using some rule, actually running them was not my intention 😀.
EDIT: I think not being able to just unsafeCoerce this makes this impossible.

[LeanderK]

I can't believe it...I've just solved it 😀 Eliminators is awesome!!

data Dict ctxt where
    Dict :: ctxt => Dict ctxt

type TypeClassInduction a (f :: [Type] -> Type) (t :: Type -> Constraint) (n :: Nat)
    = Dict (t (f (Replicate n a)))

-- due to https://ghc.haskell.org/trac/ghc/ticket/11715 we can't generate it
data TypeClassInductionSym0 :: k ~> ([Type] -> Type) ~> (Type -> Constraint) ~> Nat ~> Type
data TypeClassInductionSym1 :: k -> ([Type] -> Type) ~> (Type -> Constraint) ~> Nat ~> Type
data TypeClassInductionSym2 :: k -> ([Type] -> Type) -> (Type -> Constraint) ~> Nat ~> Type
data TypeClassInductionSym3 :: k -> ([Type] -> Type) -> (Type -> Constraint) -> Nat ~> Type
type instance Apply  TypeClassInductionSym0 a          = TypeClassInductionSym1 a
type instance Apply (TypeClassInductionSym1 a) f       = TypeClassInductionSym2 a f
type instance Apply (TypeClassInductionSym2 a  f) t    = TypeClassInductionSym3 a f t
type instance Apply (TypeClassInductionSym3 a  f  t) n = TypeClassInduction     a f t n

typeClassInduction :: forall (n :: Nat) (a :: Type) (f :: [Type] -> Type) (t :: Type -> Constraint). 
    (SingI n, t (f '[]), (t a)) 
    => (forall xs x. Dict (t (f xs)) -> Dict (t x) -> Dict (t (f (x ': xs)))) -> TypeClassInduction a f t n
typeClassInduction cStep = elimNat @(TypeClassInductionSym3 a f t) @n (sing @Nat @n) base step
        where
            base :: TypeClassInduction a f t 0
            base = Dict @(t (f (Replicate 0 a)))
    
            step :: forall (k :: Nat).
                Sing k 
                -> TypeClassInduction a f t k
                -> TypeClassInduction a f t (k :+ 1)
            step _ prev = case replicateSucc @k @a of
                        Refl -> (cStep prev (Dict @(t a)))

usage

newtype HoHeList (n :: Nat) a = HoHeList
    { unHoHeList :: HList (Replicate n a)
    }

instance (SingI n, Show a) => Show (HoHeList (n :: Nat) a) where
    show :: forall xs. xs ~ (Replicate n a) => HoHeList n a -> String
    show homogenous = let unhom :: HList xs = unHoHeList homogenous in
        case typeClassInduction @n @a @HList @Show constrStep of
            Dict -> show unhom
        where 
            constrStep :: forall (a :: Type) (ts :: [Type]). 
                Dict (Show (HList ts)) -> Dict (Show a) -> Dict (Show (HList (a : ts)))
            constrStep Dict Dict = Dict

ghci

*V2.HList> vals = 1 :&: 2 :&: 3 :&: HNil
*V2.HList> proveHomogenous vals
1:&:2:&:3:&:[]
*V2.HList> :t proveHomogenous vals
proveHomogenous vals :: Num t1 => HoHeList 3 t1
*V2.HList> hohe = proveHomogenous vals
*V2.HList> show hohe
"1:&:2:&:3:&:[]"

I just needed a bit of...creativity 😀 unbelievable that this works

EDIT: Do you know what actually happens when I run typeClassInduction? The types all make sense...but I don't know whether the code actually does something.

[RyanGlScott]

While I'm glad you found a solution, it now occurs to me that this is all completely overkill for the problem you're trying to solve. The root of the issue is that you have these two Show instances for HList:

instance (Show (HList '[])) where
    show _ = "[]"

instance (Show a, Show (HList ts)) => (Show (HList (a : ts))) where
    show (a :&: rest) = show a ++ ":&:" ++ show rest

These will only ever apply if you know statically that an HList is empty or headed by (:). But that's not the case in your Show instance for HoHeList, which is why you were struggling to define it.

If I may, I'd like to propose a much simpler solution that doesn't use eliminators at all:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Foo where

import Data.Kind
import Data.Singletons.Prelude.List
import GHC.TypeNats

data HList (ts :: [Type]) where
    HNil :: HList '[]
    (:&:) :: t -> HList ts -> HList (t ': ts)

infixr 5 :&:

type family AllC (f :: Type -> Constraint) (xs :: [Type]) :: Constraint where
  AllC _ '[]    = ()
  AllC f (x:xs) = (f x, AllC f xs)

deriving instance AllC Show xs => Show (HList xs)

newtype HoHeList (n :: Nat) a = HoHeList
    { unHoHeList :: HList (Replicate n a)
    }

deriving instance AllC Show (Replicate n a) => Show (HoHeList n a)

The key here is in the use of AllC. With this, you can define a single Show instance for all HLists, which makes defining a Show instance for HoHeList trivial. (You'll have to enable UndecidableInstances for this trick to work, but whatever.)

Now maybe some day we can define AllC by means of a type-level eliminator, but for the time being, you'll have to do the dirty work of defining it by direct recursion.

[RyanGlScott]

Do you know what actually happens when I run typeClassInduction? The types all make sense...but I don't know whether the code actually does something.

It certainly does something: it computes a Dict—linearly in the size of n, I might add. In other dependently typed languages, this might take constant time, since you could have an eta rule that says that all terms of type Dict reduce to the Dict constructor, but GHC does not have this ability due to the possibility of nontermination.

[LeanderK]

Well, at least I learned something!

Here's something interesting: At least in GHCi, printing a HoHeList 2000 Nat-List using my eliminator-based formulation is not noticeably slower than printing a replicate 2000 1-list. But the normal Show, without your formulation, is super slow (it nearly crashes for me on a 2000 vector and consumes A LOT of memory (gigabytes!). It seems that the memory does grow exponential or at least has a big coefficient in front of it).

If I am not building first the type-level list and then convert it to a HoHeList, but instead use

replicateH2 :: SNat n -> a -> HoHeList n a
replicateH2 n a =
    HoHeList (unsafeCoerce (iterate (unsafeCoerce . (a :&:)) HNil
                !! fromInteger (fromSing n)))

and then show it, I don't notice any slowdown between the eliminator-based show definition and not using not a type-level list. I can print homMany = replicateH2 (sing @Nat @200000) 1.

I have not tested your approach yet and I don't have time until tomorrow, but I think it would require building the actual type-level list.

EDIT: Since I have a Functor instance on my HoHeList (stupid name 😀 ), also printing (+1) <$> homMany seems IO-Bound. I am using these "proofs" and no Rewrite-Rules that eliminate them (seems like I don't need them?). They don't seem to not need noticable more space with increasing the HoHeList size (coDomainMatches is similiar formulated). At least I don't notice any, which is fine for now.

domainMatches :: forall (n :: Nat) (a :: Type) (b :: Type). SingI n => ToDomain (Replicate n (a -> b)) :~: Replicate n a
domainMatches = elimNat @(WhyDomainMatchesSym2 a b) @n (sing @Nat @n) base step
            where
                base :: WhyDomainMatches a b 0
                base = Refl
        
                step :: forall (k :: Nat).
                    Sing k 
                    -> WhyDomainMatches a b k 
                    -> WhyDomainMatches a b (k :+ 1)
                step _ = case replicateSucc @k @(a -> b) of
                            Refl -> case replicateSucc @k @a of
                                Refl -> cong @_ @_ @((:$$) a)

This seems like a great opportunity for trying to figure out what GHC is doing (for the first time).

EDIT 2: yeah, deriving instance AllC Show (Replicate n a) => Show (HoHeList n a)evaluates the whole list. There may be even smarter ways to implement this, but for now I am satisfied with my solution.

[LeanderK]

Am I abusing the github ticket-system in your view? Is this even interesting to you?

[RyanGlScott]

I don't think this is abusing GitHub at all! This stuff is far from obvious (both from a GHC programmer's perspective, and from the perspective of someone accustomed to dependent types in other languages).

I can't say I'm surprised to learn that code using elimNat is inefficient—you're likely seeing the combined effect of inefficient Natural code plus a complete lack of fusion that you're likely accustomed to for most data types, like lists. This library was intended to be a proof of concept, after all, and not a blazing-fast reference implementation! :)

If you're convinced that your proofs are correct, you can always make a rewrite RULE to zap it away at runtime:

{-# RULES "typeClassInductionTerminates" typeClassInduction x = unsafeCoerce Dict #-}

I can't guarantee that's the only bottleneck in your code, but it would at least remove an obvious culprit.

[LeanderK]

I think you misunderstood me (or I wasn't very clear)!
At least I was surprised how fast elimNat is. This is working:

> homMany = replicateH2 (sing @Nat @200000) 1
> homMany
(just prints a lot of 1s)
> (+1) <$> homMany
(just prints a lot of 2s)
> foldr (+) 0 homMany
20000

(all 3 are using elimNat)
where

replicateH2 :: SNat n -> a -> HoHeList n a
replicateH2 n a =
    HoHeList (unsafeCoerce (iterate (unsafeCoerce . (a :&:)) HNil
                !! fromInteger (fromSing n)))

to avoid actually building the type-level list. Having a type-level list of more than 2000 Elements starts eating all my RAM (so actually evaluating Replicate 2000 Nat). I think I stopped at GHC using 10GB Ram.

I don't notice any slowdown compared to the just calling replicate without type level stuff when using large lists.