East of Eden: Parallel Functional Programming in Idris

East of Eden: Parallel Functional Programming in Idris | Research Square window.SnipcartSettings = { analytics: { enabled: false } }; (function() { var accessVector = localStorage.getItem('access_vector') || ''; window.dataLayer = window.dataLayer || []; if (accessVector) { window.dataLayer.push({ user: { profile: { profileInfo: { snid: accessVector } } } }); } })(); (function(w,d,s,l,i){w[l]=w[l]||[];w[l].push({'gtm.start':new Date().getTime(),event:'gtm.js'});var f=d.getElementsByTagName(s)[0],j=d.createElement(s),dl=l!='dataLayer'?'&l='+l:'';j.async=true;j.src='https://www.googletagmanager.com/gtm.js?id='+i+dl;f.parentNode.insertBefore(j,f);})(window,document,'script','dataLayer','GTM-K279D39R'); Browse Preprints In Review Journals COVID-19 Preprints AJE Video Bytes Research Tools Research Promotion AJE Professional Editing AJE Rubriq About Preprint Platform In Review Editorial Policies Our Team Advisory Board Help Center Sign In Submit a Preprint Cite Share Download PDF Research Article East of Eden: Parallel Functional Programming in Idris Christopher Brown, Adam Barwell This is a preprint; it has not been peer reviewed by a journal. https://doi.org/ 10.21203/rs.3.rs-7753252/v1 This work is licensed under a CC BY 4.0 License Status: Under Review Version 1 posted 9 You are reading this latest preprint version Abstract Implicit parallel programming models typically give less parallelism control to the programmer, but require less specialised expertise. Explicit parallel models, on the other hand, give much greater parallelism control, but can require significant expertise from the programmer. In this paper, we introduce a novel semi-implicit parallel model, called Elysium, for Idris. Elysium therefore demonstrates semi-explicit parallelism for an emerging class of languages known as dependently-typed languages. These dependently-typed languages encourage safer software via their ability to express strong logical guarantees, in the form of proofs, directly in code.Our semi-implicit approach is based on a process model that uses dependent types to guarantee parallelism properties. We demonstrate how we can use this semi-implicit process model to build common algorithmic skeletons, including farms, pipelines and divide and conquer skeletons. We evaluate our process skeleton approach on a number of examples, achieving speedups of up to 22 on a 28-core machine. Idris parallelism dependent types concurrency skeletons implicit explicit processes Full Text Additional Declarations No competing interests reported. Cite Share Download PDF Status: Under Review Version 1 posted Reviews received at journal 18 Jan, 2026 Reviewers agreed at journal 12 Jan, 2026 Reviewers agreed at journal 06 Jan, 2026 Reviews received at journal 25 Nov, 2025 Reviewers agreed at journal 29 Oct, 2025 Reviewers invited by journal 29 Oct, 2025 Editor assigned by journal 28 Oct, 2025 Submission checks completed at journal 04 Oct, 2025 First submitted to journal 30 Sep, 2025 You are reading this latest preprint version Research Square lets you share your work early, gain feedback from the community, and start making changes to your manuscript prior to peer review in a journal. As a division of Research Square Company, we’re committed to making research communication faster, fairer, and more useful. We do this by developing innovative software and high quality services for the global research community. Our growing team is made up of researchers and industry professionals working together to solve the most critical problems facing scientific publishing. Also discoverable on Platform About Our Team In Review Editorial Policies Advisory Board Help Center Resources Author Services Accessibility API Access RSS feed Manage Cookie Preferences © Research Square 2026 | ISSN 2693-5015 (online) Privacy Policy Terms of Service Do Not Sell My Personal Information {"props":{"pageProps":{"initialData":{"identity":"rs-7753252","acceptedTermsAndConditions":true,"allowDirectSubmit":false,"archivedVersions":[],"articleType":"Research Article","associatedPublications":[],"authors":[{"id":541856017,"identity":"457e1537-8e73-47c0-8664-9729b806e00b","order_by":0,"name":"Christopher Brown","email":"data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAZAAAAAyAQMAAABI0h/eAAAABlBMVEX///8AAABVwtN+AAAACXBIWXMAAA7EAAAOxAGVKw4bAAAA50lEQVRIie2RsQrCMBCGTwK6BLJe8SUiguDUV0koOFXnDlLi0kdwUXwM50igLnVXstTFqYOjLmrFwUHa6uaQbzqO+7j7OQCH4y+hrVxErxLfXV2rEJ5nr+mvlbZ3TH5R2HynUa7iGDq7jY0i40PH5IRm1QraieBybRDoJBhmmZGKjjih+2qFd0Mu5Fqjr8OBN0usAAiB0HO9ouUyRmBFqdysXxaNSk9JRRDwuUXZlsLnlprDyiwBiNR4Cov+UKV3meCJb5Y18dlivL1epjEDFvYOajryGQuOeZFWK5+0oeGRDofD4WjmAQHBTolopcKwAAAAAElFTkSuQmCC","orcid":"","institution":"University of St Andrews","correspondingAuthor":true,"prefix":"","firstName":"Christopher","middleName":"","lastName":"Brown","suffix":""},{"id":541856018,"identity":"c81befbd-a2cb-4224-aa83-65c84d976c63","order_by":1,"name":"Adam Barwell","email":"","orcid":"","institution":"University of St Andrews","correspondingAuthor":false,"prefix":"","firstName":"Adam","middleName":"","lastName":"Barwell","suffix":""}],"badges":[],"createdAt":"2025-09-30 15:53:36","currentVersionCode":1,"declarations":"","doi":"10.21203/rs.3.rs-7753252/v1","doiUrl":"https://doi.org/10.21203/rs.3.rs-7753252/v1","draftVersion":[],"editorialEvents":[],"editorialNote":"","failedWorkflow":false,"files":[{"id":95542571,"identity":"a9caa079-97b1-41b5-93c6-f8c6c4984df9","added_by":"auto","created_at":"2025-11-10 11:52:50","extension":"json","order_by":0,"title":"","display":"","copyAsset":false,"role":"acdc-reference","size":3638,"visible":true,"origin":"","legend":"","description":"","filename":"fc36059ad2bd45d790bc95038daf1f23.json","url":"https://assets-eu.researchsquare.com/files/rs-7753252/v1/880338598f321c6164770a13.json"},{"id":95654722,"identity":"a675d3af-910c-4c1a-a1ce-2eb87265cf03","added_by":"auto","created_at":"2025-11-11 16:12:50","extension":"pdf","order_by":1,"title":"","display":"","copyAsset":false,"role":"manuscript-pdf","size":367109,"visible":true,"origin":"","legend":"","description":"","filename":"HLPP2025.pdf","url":"https://assets-eu.researchsquare.com/files/rs-7753252/v1_covered_2853b41a-59fa-420d-8ad8-5e2716f6f3e5.pdf"}],"financialInterests":"No competing interests reported.","formattedTitle":"East of Eden: Parallel Functional Programming in Idris","fulltext":[],"fulltextSource":"","fullText":"","funders":[],"hasAdminPriorityOnWorkflow":false,"hasManuscriptDocX":false,"hasOptedInToPreprint":true,"hasPassedJournalQc":"","hasAnyPriority":false,"hideJournal":false,"highlight":"","institution":"","isAcceptedByJournal":true,"isAuthorSuppliedPdf":true,"isDeskRejected":"","isHiddenFromSearch":false,"isInQc":false,"isInWorkflow":false,"isPdf":true,"isPdfUpToDate":true,"isWithdrawnOrRetracted":false,"journal":{"display":true,"email":"[email protected]","identity":"international-journal-of-parallel-programming","isNatureJournal":false,"hasQc":true,"allowDirectSubmit":false,"externalIdentity":"ijpp","sideBox":"Learn more about [International Journal of Parallel Programming](http://link.springer.com/journal/10766)","snPcode":"10766","submissionUrl":"https://submission.nature.com/new-submission/10766/3","title":"International Journal of Parallel Programming","twitterHandle":"","acdcEnabled":true,"dfaEnabled":true,"editorialSystem":"em","reportingPortfolio":"Springer Hybrid","inReviewEnabled":true,"inReviewRevisionsEnabled":false},"keywords":"Idris, parallelism, dependent types, concurrency, skeletons, implicit, explicit, processes","lastPublishedDoi":"10.21203/rs.3.rs-7753252/v1","lastPublishedDoiUrl":"https://doi.org/10.21203/rs.3.rs-7753252/v1","license":{"name":"CC BY 4.0","url":"https://creativecommons.org/licenses/by/4.0/"},"manuscriptAbstract":"Implicit parallel programming models typically give less parallelism control to the programmer, but require less specialised expertise. Explicit parallel models, on the other hand, give much greater parallelism control, but can require significant expertise from the programmer. In this paper, we introduce a novel semi-implicit parallel model, called Elysium, for Idris. Elysium therefore demonstrates semi-explicit parallelism for an emerging class of languages known as dependently-typed languages. These dependently-typed languages encourage safer software via their ability to express strong logical guarantees, in the form of proofs, directly in code.Our semi-implicit approach is based on a process model that uses dependent types to guarantee parallelism properties. We demonstrate how we can use this semi-implicit process model to build common algorithmic skeletons, including farms, pipelines and divide and conquer skeletons. We evaluate our process skeleton approach on a number of examples, achieving speedups of up to 22 on a 28-core machine.","manuscriptTitle":"East of Eden: Parallel Functional Programming in Idris","msid":"","msnumber":"","nonDraftVersions":[{"code":1,"date":"2025-11-10 11:52:45","doi":"10.21203/rs.3.rs-7753252/v1","editorialEvents":[{"type":"communityComments","content":0},{"type":"editorInvitedReview","content":"","date":"2026-01-18T17:16:46+00:00","index":"hide","fulltext":""},{"type":"reviewerAgreed","content":"275223869792509314200631202508278876786","date":"2026-01-12T12:34:59+00:00","index":"hide","fulltext":""},{"type":"reviewerAgreed","content":"146678469633285254820533571710069210738","date":"2026-01-06T16:44:38+00:00","index":"hide","fulltext":""},{"type":"editorInvitedReview","content":"","date":"2025-11-25T08:50:28+00:00","index":"hide","fulltext":""},{"type":"reviewerAgreed","content":"203620252831739862547946578736529335781","date":"2025-10-29T17:33:41+00:00","index":"hide","fulltext":""},{"type":"reviewersInvited","content":"","date":"2025-10-29T07:31:02+00:00","index":"","fulltext":""},{"type":"editorAssigned","content":"","date":"2025-10-28T09:46:39+00:00","index":"","fulltext":""},{"type":"checksComplete","content":"","date":"2025-10-04T08:42:26+00:00","index":"","fulltext":""},{"type":"submitted","content":"International Journal of Parallel Programming","date":"2025-09-30T15:42:48+00:00","index":"","fulltext":""}],"status":"published","journal":{"display":true,"email":"[email protected]","identity":"international-journal-of-parallel-programming","isNatureJournal":false,"hasQc":true,"allowDirectSubmit":false,"externalIdentity":"ijpp","sideBox":"Learn more about [International Journal of Parallel Programming](http://link.springer.com/journal/10766)","snPcode":"10766","submissionUrl":"https://submission.nature.com/new-submission/10766/3","title":"International Journal of Parallel Programming","twitterHandle":"","acdcEnabled":true,"dfaEnabled":true,"editorialSystem":"em","reportingPortfolio":"Springer Hybrid","inReviewEnabled":true,"inReviewRevisionsEnabled":false}}],"origin":"","ownerIdentity":"df139a2c-5932-40e1-a91b-0edcc3be9a90","owner":[],"postedDate":"November 10th, 2025","published":true,"recentEditorialEvents":[],"rejectedJournal":[],"revision":"","amendment":"","status":"under-review","subjectAreas":[],"tags":[],"updatedAt":"2026-02-24T05:25:10+00:00","versionOfRecord":[],"versionCreatedAt":"2025-11-10 11:52:45","video":"","vorDoi":"","vorDoiUrl":"","workflowStages":[]},"version":"v1","identity":"rs-7753252","journalConfig":"researchsquare"},"__N_SSP":true},"page":"/article/[identity]/[[...version]]","query":{"redirect":"/article/rs-7753252","identity":"rs-7753252","version":["v1"]},"buildId":"8U1c8b4HqxoKbykW_rLl7","isFallback":false,"isExperimentalCompile":false,"dynamicIds":[84888],"gssp":true,"scriptLoader":[]}