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  6490 reads

Browse archivesActive forum topics 
Recent comments
22 min 7 sec ago
1 hour 21 min ago
2 hours 48 min ago
3 hours 19 sec ago
3 hours 52 min ago
5 hours 27 min ago
7 hours 2 min ago
7 hours 19 min ago
13 hours 40 min ago
15 hours 36 min ago