User loginNavigation 
What is this type of type called?Often restricted data types are used as jails. For example, the IO monad in Haskell can't let any impure value escape. Sometimes however, even though it is not safe to release any value from the jail in general it is possible for some specific values. As an example, for some type T one might want to allow a function of the type "(T a > T b) > (a > b)", but not a function of the type "T a > a". Another example, which is trivial, is that one might allow data of the type,(using Coq's notation for types where the values are constrained by propositions), "{ x : IO a  forsome y, x = pure y }" to escape where pure is the function of the type "a > IO a". What is it called when a data type can't be extracted from but a more complex data type built up from it can? By Steven StewartGallus at 20111215 18:54  LtU Forum  previous forum topic  next forum topic  other blogs  6362 reads

Browse archivesActive forum topics 
Recent comments
3 days 17 hours ago
1 week 4 days ago
2 weeks 1 hour ago
2 weeks 1 hour ago
2 weeks 1 hour ago
2 weeks 2 hours ago
2 weeks 3 hours ago
2 weeks 4 hours ago
2 weeks 8 hours ago
2 weeks 10 hours ago