Copyright	Copyright (C) 2015 Kyle Carter
License	BSD3
Maintainer	Kyle Carter <kylcarte@indiana.edu>
Stability	experimental
Portability	RankNTypes
Safe Haskell	None
Language	Haskell2010

Data.Type.Option

Description

A type combinator for type-level Maybes, lifting (f :: k -> *) to (Option f :: Maybe k -> *).

Synopsis

Documentation

data Option f :: Maybe k -> * where Source

Constructors

Nothing_ :: Option f Nothing
Just_ :: !(f a) -> Option f (Just a)

Instances

(Witness p q (f a), (~) (Maybe k) x (Just k a)) => Witness p q (Option k f x) Source
Traversable1 k (Maybe k) (Option k) Source
Foldable1 k (Maybe k) (Option k) Source
Functor1 k (Maybe k) (Option k) Source	We can take a natural transformation of `(forall x. f x -> g x)` to a natural transformation of `(forall mx. Option f mx -> Option g mx)`.
Known (Maybe k) (Option k f) (Nothing k) Source
Known k f a => Known (Maybe k) (Option k f) (Just k a) Source
type WitnessC p q (Option k f x) = Witness p q (f (FromJust k x)) Source
type KnownC (Maybe k) (Option k f) (Nothing k) = ØC
type KnownC (Maybe k) (Option k f) (Just k a) = Known k f a Source

option :: (forall a. (m ~ Just a) => f a -> r) -> ((m ~ Nothing) => r) -> Option f m -> r Source

Eliminator for Option f.