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.
NB: the result type of the eliminating function may
not refer to the universally quantified type index a
.
This function deserves more documentation. It is a powerful basis for working with correct-by-construction data. 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.