Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Can you do pattern matching on the type-level in Haskell?

Basically, what I want is a function that takes a function type (a -> b -> c -> ...), and returns a list of all the right-subset types of that function type, for example, lets call this function f:

x = f (a -> b -> c)

x
> [a -> b -> c, b -> c, c]

And this should work for both polymorphic types, as in my example, and on concrete function types.

This would be relatively straightforward if you could pattern match on the type-level with function types like so:

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

used as a utility function for the construction of f above, and pattern matching over function types sort of like one would pattern match over a list.

like image 212
Nathan BeDell Avatar asked Aug 15 '14 15:08

Nathan BeDell


1 Answers

Closed type families are what you're 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 type-level lists too:

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

type family F a :: [*] where
    F (x -> xs) = (x -> xs) ': (F xs)
    F x         = '[x]

The single quote indicates that we are using those (list) constructors at a type level.

We can see that this gives the expected result with the :kind! command in GHCi

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

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

Untagged sum types

Regarding the full context: You might be able to make something like an untagged sum type by making an Elem type family using the type level (==) and (||) from Data.Type.Equality and Data.Type.Bool respectively.

like image 136
David Young Avatar answered Sep 21 '22 13:09

David Young