CODEWITHSUNDEEP
haskell
RandomB
RandomB

Reputation: 3747

Filtering on type-level

Consider, I have types-markers:

data Uniq = Uniq deriving Show
data NUniq = NUniq deriving Show
data UUniq = UUniq deriving Show

and predicate to distinguish them:

type family IsMark a :: Bool
type instance IsMark Uniq = 'True
type instance IsMark NUniq = 'True
type instance IsMark UUniq = 'True

and "convertor" from '[A, B, ..] to A -> B -> ..:

type Id x = x
type Fn x y = x -> y

type family TL2Fun xs where
  TL2Fun '[x] = Id x
  TL2Fun (x ': xs) = Fn x (TL2Fun xs)

so this signature is right:

f1 :: TL2Fun '[Int, Int, Int]
f1 a b = a + b

Now I want this:

f2 :: TL2Fun (WOMarks '[Int, Int, Int, Uniq])
f2 a b = a + b

i.e. filter-out Uniq from this list first. So, I add filter function based on my predicate:

type family WOMarks xs where
  WOMarks '[] = '[]
  WOMarks (x ': xs) = If (IsMark x) (WOMarks xs) (x ': (WOMarks xs))

where If is imported from Data.Type.Bool (or I can implement it with PolyKind)...

But f2 is not compiling, I get error like

 • Couldn't match type ‘TL2Fun
                          (If
                             (IsMark Int)
                             (If
                                (IsMark Int)
                                (If (IsMark Int) '[] '[Int])
                                (Int : If (IsMark Int) '[] '[Int]))
                             (Int
                                : If
                                    (IsMark Int)
                                    (If (IsMark Int) '[] '[Int])
                                    (Int : If (IsMark Int) '[] '[Int])))’
                  with ‘a0 -> a0 -> a0’
   Expected type: TL2Fun (WOMarks '[Int, Int, Int, Uniq])
     Actual type: a0 -> a0 -> a0
   The type variable ‘a0’ is ambiguous
 • The equation(s) for ‘f2’ have two arguments,
   but its type ‘TL2Fun (WOMarks '[Int, Int, Int, Uniq])’ has none (intero)

which looks like If exists in my filtering attempt: it's tree of "calls", but it was not "evaluated" to filtered result (or something else, I'm not sure about error reason). How to achieve my goal, ie, to remove types by predicate?

Upvotes: 1

Views: 66

Answers (1)

K. A. Buhr
K. A. Buhr

Reputation: 50864

As was noted by @M.Aroosi, you need an instance of IsMark for Int:

type instance IsMark Int = 'False

after which the program will type check. Of course, you don't want to have to define an instance for every non-mark type, and using:

type instance IsMark a = 'False

will lead to conflicting instances.

The solution is to define a closed type family instead:

type family IsMark a :: Bool where
  IsMark Uniq = 'True
  IsMark NUniq = 'True
  IsMark UUniq = 'True
  IsMark a = 'False

after which it should all work:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Type.Bool

data Uniq = Uniq deriving Show
data NUniq = NUniq deriving Show
data UUniq = UUniq deriving Show

type family IsMark a :: Bool where
  IsMark Uniq = 'True
  IsMark NUniq = 'True
  IsMark UUniq = 'True
  IsMark a = 'False

type Id x = x
type Fn x y = x -> y

type family TL2Fun xs where
  TL2Fun '[x] = Id x
  TL2Fun (x : xs) = Fn x (TL2Fun xs)

f1 :: TL2Fun '[Int, Int, Int]
f1 a b = a + b

type family WOMarks xs where
  WOMarks '[] = '[]
  WOMarks (x : xs) = If (IsMark x) (WOMarks xs) (x : (WOMarks xs))

f2 :: TL2Fun (WOMarks '[Int, Int, Int, Uniq])
f2 a b = a + b

Upvotes: 3

Related Questions