Quantified Constraint and Case Analysis

Learn
#1

Is there a way to do case analysis such that it unifies with a quantified constraint? For example

data Cases x = A x | B x | C x

casesAnalisis :: forall (psi :: Types -> Constraint) r.
  ( forall x. psi (A x)
  , forall x. psi (B  x)
  , forall x. psi (C x)
  ) => (forall (x :: Cases). (psi x) => r) -> r
casesAnalisis f = f
#2

I think what you probably want is the below. Does that satisfy your needs?

N.B. you really will need Typeable otherwise you’re never really going to be able to do anything with the constraints you have. There are very few phis that satisfy forall x. psi (A x) but many interesting ones that satisfy forall x. Typeable x => psi (A x)!

{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE NoStarIsType #-}
{-# OPTIONS_GHC -Wall #-}

-- requires packages: singletons, constraints

import Data.Constraint (Dict (Dict))
import Data.Kind (Constraint, Type)
import Data.Proxy (Proxy (Proxy))
import Data.Singletons (Sing, SingI, sing)
import Data.Typeable (Typeable)
import Type.Reflection (someTypeRep)

type Cases :: Type -> Type
data Cases x = A x | B x | C x

-- {

-- This singletons stuff is mechanical, and can (in theory) be
-- autogenerated.  Perhaps singletons-th does it?

type SCases :: forall (x :: Type) -> Cases x -> Type
data SCases x c where
  SA :: (Typeable t) => SCases x (A t)
  SB :: (Typeable t) => SCases x (B t)
  SC :: (Typeable t) => SCases x (C t)

type instance Sing @(Cases x) = SCases x

instance (Typeable x) => SingI (A x) where
  sing = SA

instance (Typeable x) => SingI (B x) where
  sing = SB

instance (Typeable x) => SingI (C x) where
  sing = SC

-- }

caseAnalysis ::
  forall (x :: Type) (psi :: Cases x -> Constraint) (y :: Cases x).
  ( forall x'. (Typeable x') => psi (A x'),
    forall x'. (Typeable x') => psi (B x'),
    forall x'. (Typeable x') => psi (C x'),
    SingI y
  ) =>
  Dict (psi y)
caseAnalysis = case sing @y of
  SA -> Dict
  SB -> Dict
  SC -> Dict

class CC (t :: Cases x) where
  showCImpl :: Proxy t -> String

showC :: forall t. (CC t) => String
showC = showCImpl (Proxy @t)

showTypeable :: forall t. (Typeable t) => String
showTypeable = show (someTypeRep (Proxy @t))

instance (Typeable x) => CC (A x) where
  showCImpl _ = "A " ++ showTypeable @x

instance (Typeable x) => CC (B x) where
  showCImpl _ = "B " ++ showTypeable @x

instance (Typeable x) => CC (C x) where
  showCImpl _ = "C " ++ showTypeable @x

usage :: (SingI y) => Dict (CC y)
usage = caseAnalysis

-- > example
-- "A 5"
example :: String
example = case usage @(A 5) of Dict -> showC @(A 5)
1 Like
#3

That’s what I was looking for!

I was too invested in the continuation to see that I could achieve the same by creating the Dict explicitly.

Also thanks for the extra info! I’m currently using the singletons package :).

1 Like