Difference between revisions of "Talk:Open research problems"

From HaskellWiki
Jump to navigation Jump to search
m
(I/O-related content relocated to "Talk:The I/O quandary")
 
(One intermediate revision by the same user not shown)
Line 1: Line 1:
  +
There is currently no text in this page.
== Denotative languages and the I/O problem ==
 
  +
You can <span style="color:brown;">search for this page title</span> in other pages,
 
  +
<span style="color:brown;">search the related logs</span>,
<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
  +
or <span style="color:brown;">create this page</span>.
My view is that the next logical step for programming is to split into two non-overlapping programming domains:
 
 
* runtime building for …
 
* … mathematical programming languages
 
 
<tt>[https://www.haskellforall.com/2021/04/the-end-of-history-for-programming.html Gabriella Gonzalez].</tt>
 
</div>
 
 
Let's assume:
 
* a denotative language exists - here, it's called <i>DL</i>.
 
* the implementation of <i>DL</i> is written in an imperative language - let's call that <i>IL</i>.
 
 
Let's also assume:
 
* <i>DL</i> is initially successfull.
 
* solid-state Turing machines remain in use, so <i>IL</i> is still needed.
 
 
As time goes on, technology advances which means an ever-expanding list of hardware to cater for. Unfortunately, the computing architecture remains mired in state and effects - supporting the new hardware usually means a visit to <i>IL</i> to add the extra subroutines/procedures (or modify existing ones) in the implementation.
 
 
<i>DL</i> will still attract some interest:
 
 
* Parts of the logic required to support hardware can be more usefully written as <i>DL</i> definitions, to be called by the implementation where needed - there's no problem with imperative code calling denotative code.
 
 
* periodic refactoring of the implementation reveals suitable candidates for replacement with calls to <i>DL</i> expressions.
 
 
* <i>DL</i> is occasionally extended to cater for new patterns of use - mostly in the form of new abstractions and their supporting libraries, or (more rarely) the language itself and therefore its implementation in <i>IL</i>.
 
 
...in any case, <i>DL</i> remains denotative - if you want a computer to do something new to its surroundings, that usually means using <i>IL</i> to modify the implementation of <i>DL</i>.
 
 
So the question is this: which language will programmers use more often, out of habit - <i>DL</i> or <i>IL</i>?
 
 
Here's a clue:
 
 
<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
 
They [monadic types] are especially useful for structuring large systems. In fact, there's a danger of programming in this style too much (I know I do), and almost forgetting about the 'pure' style of Haskell.
 
 
<tt>[[Monad tutorials timeline|Noel Winstanley]].</tt>
 
</div>
 
 
Instead of [http://conal.net/blog/posts/can-functional-programming-be-liberated-from-the-von-neumann-paradigm looking at the whole system in a consistently denotational style (with simple & precise semantics)] by using <i>DL</i> alone, most users would be working on the implementation using <i>IL</i> - being denotative makes for nice libraries, but getting the job done means being imperative. Is this an improvement over the current situation in Haskell? No - instead of having the denotative/imperative division in Haskell by way of types, users would be contending with that division <i>at the language level</i> in the forms of differing syntax and semantics, annoying foreign calls, and so forth.
 
 
The advent of Haskell's FFI is an additional aggravation - it allows countless more effect-centric operations to be accessed. Moving <b>all</b> of them into a <i>finite</i> implementation isn't just impractical - it's impossible.
 
 
But if you still think being denotative is worth all that bother (or you just want to prove me wrong :-) [https://www.ioccc.org/2019/lynn/hint.html this] could be a useful place to start:
 
 
<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
* <tt>OneHundredPercentPure</tt>: Gone is the catch-all lawless <code>IO</code> monad. And no trace of those scary <code>unsafeThisAndThat</code> functions. All functions must be pure.
 
</div>
 
 
&mdash; [[User:Atravers|Atravers]] Fri Oct 22 06:36:41 UTC 2021
 
 
 
== Outsourcing the I/O problem ==
 
 
<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
'''4 Compiling Agda programs'''
 
 
This section deals with the topic of getting Agda programs to interact
 
with the real world. Type checking Agda programs requires evaluating
 
arbitrary terms, ans as long as all terms are pure and normalizing this is
 
not a problem, but what happens when we introduce side effects? Clearly,
 
we don't want side effects to happen at compile time. Another question is
 
what primitives the language should provide for constructing side effecing
 
programs. In Agda, these problems are solved by <i>allowing arbitrary
 
Haskell functions to be imported as axioms.</i> At compile time, these imported
 
functions have no reduction behaviour, <i>only at run time is the
 
Haskell function executed</i>.
 
 
<tt>[http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf Dependently Typed Programming in Agda], Ulf Norell and James Chapman [<i>emphasis added</i>].</tt>
 
</div>
 
 
In Haskell:
 
 
* just extend the FFI enough to replace the ''usually''-abstract I/O definitions with calls to foreign definitions:
 
:{|
 
|<haskell>
 
instance Monad IO where
 
return = primUnitIO
 
(>>=) = primBindIO
 
 
foreign import ccall unsafe primUnitIO :: a -> IO a
 
foreign import ccall unsafe primBindIO :: IO a -> (a -> IO b) -> IO b
 
 
</haskell>
 
|}
 
 
* the <code>IO</code> type is then just a type-level tag, as specified in the Haskell 2010 report:
 
 
:{|
 
|<haskell>
 
data IO a -- that's all folks!
 
</haskell>
 
|}
 
 
''Voilà!'' In this example, the I/O problem has been outsourced to C - if you're not happy with C's solution to the I/O problem, just use another programming language for the Haskell implementation: there's plenty of them to choose from (...but don't use Haskell, to avoid going <code>⊥</code>-up ;-).
 
 
By defining them in this way, <code>IO</code> and its actions in Haskell can also be thought of as being "axiomatic": they have no effect when a Haskell program is compiled, only at run time is the foreign definition executed and its effects occur.
 
 
&mdash; [[User:Atravers|Atravers]] Thu Dec 9 01:55:47 UTC 2021
 
 
== Mathematics and the I/O problem ==
 
 
 
Mathematics is abstract:
 
 
<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
In a preliminary sense, mathematics is abstract because it is studied using highly general and formal resources.
 
 
<tt>[https://iep.utm.edu/math-app The Applicability of Mathematics], from the [https://iep.utm.edu/Internet Encyclopedia of Philosophy].</tt>
 
</div>
 
 
In particular, it abstracts from the existence of an external environment. This poses a challenge for languages like Haskell which pursue the mathematical notion of a function (rather than use subroutines or procedures):
 
 
<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
 
How must interactions between a program and an external environment (consisting of, e.g., input/output-devices, file systems, ...) be described in a programming language that abstracts from the existence of an outside world?
 
 
<tt>[https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.95.9846&rep=rep1&type=pdf Funtions, Frames and Interactions], Claus Reinke (page 10 of 210).</tt>
 
</div>
 
 
So the seeking of a "pure"/"mathematical"/"functional"/"formal"/... '''general-purpose''' solution to I/O which <u>isn't</u> [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.13.9123&rep=rep1&type=pdf awkward] should focus on finding an extension of mathematics which can [https://www.cs.kent.ac.uk/people/staff/dat/krc/paraffins-turner.pdf elegantly] describe interactions with external environments:
 
* If one exists, denotational semantics can then be used to map it into Haskell.
 
* If one cannot exist (like the solution to the halting problem), then implementors everywhere can just select the most-suitable (or least-ugly) model of I/O as they see fit.
 
 
&mdash; [[User:Atravers|Atravers]] Fri Jan 28 22:33:43 UTC 2022
 

Latest revision as of 07:30, 3 March 2022

There is currently no text in this page. You can search for this page title in other pages, search the related logs, or create this page.