Skip to content

Instantly share code, notes, and snippets.

@deech
Created January 8, 2016 15:28
Show Gist options
  • Save deech/8b2e835459aba3ed7bec to your computer and use it in GitHub Desktop.
Save deech/8b2e835459aba3ed7bec to your computer and use it in GitHub Desktop.
Searching a type level list using typeclasses vs. closed type families.
{-
This code shows how to check if a type-level list contains a given type.
It first shows the approach required for older versions of GHC (< 7.6.x)
and then a version using closed type families supported in GHC 7.8.1 and greater.
-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
-- The data structure used the for the examples below.
-- elements of a type level list
data A a
data B a
data C a
data D a
data E a
data F a
-- an example of a heterogenous list
type TypeLevelList = (A (B (C (D (E ())))))
-- Everything from here to the closing comment "Old way ends here"
-- shows the old way.
-- First we need to test for equality at the type level
-- so we can test if some type is what we are looking for.
data Yes
data No
class TypeEqual x y b | x y -> b
instance {-# OVERLAPPING #-} TypeEqual a a Yes
instance {-# OVERLAPPABLE #-} No ~ b => TypeEqual x y b
-- a runner that tests that the type passed in matches
-- (A ())
runTypeEqual :: (TypeEqual a (A ()) Yes) => a -> IO ()
runTypeEqual _ = print "ran!"
{-
> runTypeEqual (undefined :: (A ()))
"ran!"
> runTypeEqual (undefined :: (B ()))
<interactive>:35:1:
Couldn't match type ‘No’ with ‘Yes’
In the expression: runTypeEqual (undefined :: B ())
In an equation for ‘it’: it = runTypeEqual (undefined :: B ())
-}
-- In order ot get to the next element of the list we need to
-- pop its head.
class Tail aas as | aas -> as
instance Tail (a as) as
instance (r ~ ()) => Tail () r
-- a runner that returns the tail of a type-level list
runTail :: (Tail aas as) => aas -> as -> IO ()
runTail _ _ = print "ran!"
{-
> :t runTail (undefined :: (A (B (C (D ())))))
runTail (undefined :: (A (B (C (D ()))))) :: B (C (D ())) -> IO ()
-}
-- Now we can check if the type is in the list
class Contains' a b match r | a b match -> r
instance (Tail aas as, Contains as b r) => Contains' aas b No r
instance (r ~ Yes) => Contains' a b Yes r
class Contains as a r | as a -> r
instance (TypeEqual (a ()) b match, Contains' (a as) b match r) => Contains (a as) b r
instance Contains () b No
-- A runner that checks if the type of the argument is one of (A (B (C (D (E ())))))
runContains :: (Contains (A (B (C (D (E ()))))) a Yes) => a -> IO ()
runContains _ = print "ran!"
{-
> runContains (undefined :: B ())
"ran!"
> runContains (undefined :: F ())
<interactive>:38:1:
Couldn't match type ‘No’ with ‘Yes’
arising from a functional dependency between:
constraint ‘Contains () (F ()) Yes’
arising from a use of ‘runContains’
instance ‘Contains () b No’
at /home/deech/Haskell/TypeLevelLiterals/TypeFamily.hs:59:10-25
In the expression: runContains (undefined :: F ())
In an equation for ‘it’: it = runContains (undefined :: F ())
-}
-- Old way ends here
-- The new way with closed type families
type family ClosedContains haystack (needle :: *) where
ClosedContains (x xs) (x ()) = Yes
ClosedContains () (x ()) = No
ClosedContains (x xs) (y ()) = ClosedContains xs (y ())
-- a runner that test for type-level list membership just like 'runContains'.
runClosedContains :: (Yes ~ ClosedContains (A (B (C (D (E ()))))) a) => a -> IO ()
runClosedContains _ = print "ran!"
{-
runClosedContains (undefined :: (A ()))
"ran!"
*Main> runClosedContains (undefined :: (F ()))
<interactive>:53:1:
Couldn't match type ‘No’ with ‘Yes’
Expected type: ClosedContains (A (B (C (D (E ()))))) (F ())
Actual type: Yes
In the expression: runClosedContains (undefined :: F ())
In an equation for ‘it’: it = runClosedContains (undefined :: F ())
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment