Copyright | Copyright (C) 2015 Kyle Carter |
---|---|
License | BSD3 |
Maintainer | Kyle Carter <kylcarte@indiana.edu> |
Stability | experimental |
Portability | RankNTypes |
Safe Haskell | None |
Language | Haskell2010 |
Documentation
some :: Some f -> (forall a. f a -> r) -> r Source
An eliminator for a Some
type.
Consider this function akin to a Monadic bind, except instead of binding into a Monad with a sequent function, we're binding into the existential quantification with a universal eliminator function.
It serves as an explicit delimiter in a program of where the type index may be used and depended on, and where it may not.
NB: the result type of the eliminating function may
not refer to the universally quantified type index a
.