Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

How to map existentials with multiple constraints in Haskell?

Tags:

haskell

I figured out how to process a list of heterogeneous types constrained by a single class:

data Ex c = forall a. (c a) => Ex a

forEx :: [Ex c] -> (forall a. c a => a -> b) -> [b] 
forEx [] _ = [] 
forEx (Ex a:r) f = f a : forEx r f

> forEx @Show [Ex 3, Ex (), Ex True] show
["3","()","True"]

Looks great, but in real life instead of show function would more complicated one relying on more than 1 constraint. Going further by analogy doesn't work:

Attempt 1:

forEx @(Show, Eq) [Ex 3, Ex (), Ex True] show

<interactive>:85:8: error:
    • Expected kind ‘* -> Constraint’, but ‘(Show, Eq)’ has kind ‘*’

Attempt 2:

type ShowEq c = (Show c, Eq c)
> forEx @ShowEq [Ex 3, Ex (), Ex True] show

<interactive>:87:1: error:
    • The type synonym ‘ShowEq’ should have 1 argument, but has been given none

Attempt 3 works, but defining dummy class and instance for one time use is to clumsy:

class (Show a, Eq a) => ShowEq1 a 
instance (Show a, Eq a) => ShowEq1 a
forEx @ShowEq1 [Ex (3::Int), Ex (), Ex True] show

["3","()","True"]
like image 955
Daniil Iaitskov Avatar asked Dec 16 '21 21:12

Daniil Iaitskov


Video Answer


2 Answers

With enough language features, it's possible to make a constraint that combines constraints:

{-# LANGUAGE RankNTypes, ConstraintKinds, GADTs, TypeApplications, MultiParamTypeClasses, FlexibleInstances, UndecidableSuperClasses #-}

data Ex c = forall a. (c a) => Ex a

forEx :: [Ex c] -> (forall a. c a => a -> b) -> [b] 
forEx [] _ = [] 
forEx (Ex a:r) f = f a : forEx r f

class (c a, d a) => (Combined c d) a
instance (c a, d a) => (Combined c d) a

shown :: [String]
shown = forEx @(Combined Show Eq) [Ex 3, Ex (), Ex True] show
like image 157
Aplet123 Avatar answered Oct 18 '22 01:10

Aplet123


I would do it this way:

{-# LANGUAGE DataKinds, GADTs, RankNTypes, StandaloneKindSignatures, TypeFamilies, TypeOperators #-}

import Data.Kind

type All :: [Type -> Constraint] -> Type -> Constraint
type family All cs t
  where All '[] _ = ()
        All (c ': cs) t = (c t, All cs t)

data Ex cs
  where Ex :: All cs t => t -> Ex cs

forEx :: [Ex cs] -> (forall a. All cs a => a -> b) -> [b]
forEx [] _ = []
forEx (Ex x : xs) f = f x : forEx xs f

Now Ex is parameterised not on a single class but a list of classes1. And we have the All type family for taking a list of classes and applying them all to the same type, combining them into a single Constraint.

This means (unlike the class-to-combine-two-other-classes approach) it now supports any number of constraints you need.

You can call it like this2:

λ forEx @[Show, Eq] [Ex 3, Ex (), Ex True] show
["3","()","True"]
it :: [String]

1 Technically not a list of classes, but rather a list of things that need one more type argument to produce a Constraint. Single-param classes would be the most common thing you'd use this on, though.


2 Of course Eq is not a very useful constraint to have in there, because you can't actually use it without another value of the same unknown type, and you've thrown away all the information about whether any given type is the same type.

like image 2
Ben Avatar answered Oct 18 '22 01:10

Ben