Tutorial by Examples

The Proxy :: k -> * type, found in Data.Proxy, is used when you need to give the compiler some type information - eg, to pick a type class instance - which is nonetheless irrelevant at runtime. {-# LANGUAGE PolyKinds #-} data Proxy a = Proxy Functions which use a Proxy typically use Scoped...

Since Proxy contains no runtime information, there is never a need to pattern-match on the Proxy constructor. So a common idiom is to abstract over the Proxy datatype using a type variable. showread :: forall proxy a. (Show a, Read a) => proxy a -> String -> String showread _ = (show :: a...

Since Proxy contains no runtime information, you can always write a natural transformation f a -> Proxy a for any f. proxy :: f a -> Proxy a proxy _ = Proxy This is just like how any given value can always be erased to (): unit :: a -> () unit _ = () Technically, Proxy is the term...