Can you perform level-level pattern matching in Haskell?

Question

Basically, what I want is a function that takes a type of function (a → b → c → ...) and returns a list of all types of subtypes of this type of function, for example, it allows you to call this function f:

x = f (a -> b -> c) x > [a -> b -> c, b -> c, c] 

And this should work both for polymorphic types, and in my example, and for specific types of functions.

It would be relatively simple if you could map the image at the type level to these types of functions:

 g (x -> xs) = xs g (x) = x 

is used as a utility function to build f above, and matching patterns by function types is similar to pattern matching over a list.

Answer 1

The private type is what you are looking for:

 {-# LANGUAGE TypeFamilies #-} type family F a where F (x -> xs) = xs F x = x 

To fully answer your question, we need DataKinds to get lists of type types:

 {-# LANGUAGE TypeFamilies, TypeOperators, DataKinds #-} type family F a :: [*] where F (x -> xs) = (x -> xs) ': (F xs) F x = '[x] 

A single quote indicates that we are using these (list) constructors at the type level.

We see that this gives the expected result with the command :kind! at ghci

 λ> :kind! F (Int -> Float -> Double) F (Int -> Float -> Double) :: [*] = '[Int -> Float -> Double, Float -> Double, Double] 

Note that the return type of F is [*] . This means that in order to use these results, you will need to somehow extract them from the list. The only type that has types that are habitable is * (well, and # ).

Types without tags

Regarding the full context: Perhaps you can do something like an unlabeled sum type by creating an Elem family of types using level levels (==) and (||) from Data.Type.Equality and Data.Type.Bool respectively.