Pages

14 January 2016

Thoughts on using fractional types to model mutable borrowing of substructures

In type theory, a pair is denoted by a product type, with a constructor pair and two projections fst and snd:

$mathjax[ \textrm{pair}(a, b) : a \times b \\ \textrm{fst} : a \times b \to a \\ \textrm{snd} : a \times b \to b ]$

These projections are destructive: the pair is consumed, and one of the values is discarded. However, when we have a large structure, often it’s cheaper to modify parts of it in place, rather than duplicating and reconstructing it. So we’d like to come up with a system that lets us lend a field out for modification temporarily, and repossess the modified field afterward. That would let us model mutation in terms of pure functions, with the same performance as direct mutation.

Obviously our projections can’t destroy either of the fields, because we want to be able to put them back together into a real pair again. So the functions must be linear—the result has to contain both $mathjax(a)$ and $mathjax(b)$. What result can we return other than $mathjax(a \times b)$? I dunno, how about something isomorphic?

$mathjax[ \textrm{lend-fst} : a \times b \to a \times ((a \times b) / a) \\ \textrm{lend-snd} : a \times b \to b \times ((a \times b) / b) ]$

So this gives us a semantics for quotient types: a quotient $mathjax(a / b)$ denotes a value of type $mathjax(a)$ less a “hole” that we can fill in with a value of type $mathjax(b)$. We can implement this by drawing another isomorphism between $mathjax((a \times b) / a)$ and something like $mathjax(\textrm{ref}(a) \times (\textrm{hole}(\textrm{sizeof}(a)) \times b))$—the “hole” is an appropriately sized slot that we can fill in with a value of type $mathjax(a)$, and the quotient denotes a write-once mutable reference to that slot.

The inverses of the lending functions are the repossession functions, which repossess the field and reconstitute the pair by filling in the reference:

$mathjax[ \textrm{repo-fst} : a \times ((a \times b) / a) \to a \times b \\ \textrm{repo-snd} : b \times ((a \times b) / b) \to a \times b ]$

When we fill in the slot, the reference and quotient are destroyed, and we get back a complete data structure again. The references are relative, like C++ member references, so we could use this to implement, say, swapping fields between two structures.

I’m pretty sure that if you made these types non-duplicable, it’d guarantee that the lifetime of a substructure reference would be a sub-lifetime of the lifetime of the structure. So, notably, these lending functions wouldn’t need to actually do anything at runtime; they’d simply give us a type-level way to ensure that only one mutable reference to a particular field of a value could exist at a time. The same property is enforced in Rust with its borrow system, but in this system, we don’t need any concept of references or lifetimes. Rather than enforce a static approximation of stack/scope depth, as in Rust, we can enforce a static approximation of structure depth.

We probably need a subtyping rule, which states that a quotient type is a subtype of its numerator, as long as the denominator is not void:

$mathjax[ a / b \le a, b \ne 0 ]$

You can’t borrow a void field from a structure anyway, because you can’t construct a void value, so the side condition should never come up in practice.

In order for this to be useful in a real language, we probably need an additional “swap” rule, which states that it doesn’t matter in which order we lend or repossess substructures:

$mathjax[ a / b / c = a / c / b ]$

And clearly $mathjax(a / 1)$ is isomorphic to $mathjax(a)$, because every structure is perfectly happy to lend out useless values, and repossessing them does nothing.

We can use negative types to denote borrowing of fields from discriminated unions. If the type $mathjax(a + b)$ denotes a discriminated union like Haskell’s Either a b (which has a value of Left x where x is of type a, or Right y where y is of type b) then we also have two projections—but they’re weird:

$mathjax[ \textrm{lend-left} : a + b \to a + ((a + b) - a) \\ \textrm{lend-right} : a + b \to b + ((a + b) - b) ]$

Here, when we try to lend out a field, it might not be present. So we get either the lent field, or an instance of a smaller sum type. This can be used to implement pattern-matching: try to lend each field in turn, reducing the space of possible choices by one field at a time. If you get all the way down to $mathjax(0)$, you have a pattern-match failure. This automatically rules out redundant patterns: you can’t try to match on a field you’ve already tried, because it’s no longer present in the type.

That’s about as far as I’ve gotten with this line of thinking. If anyone has ideas for how to extend it or put it into practice, feel free to comment.

54 comments:

  1. There is no real formula that can tell anyone how the industry is going to innovate and develop in the future, whether this is in telecom, labor or gig economy. However, the future of field engineering is changing all the time, because technology is constantly evolving. With evolving technology, Field Engineers are facing a future where their career is going to adapt, and they must be ready to embrace those changes.
    future of engineering

    ReplyDelete
  2. Hi Nice Post,
    I work as a marketing specialist and staff author at Externetworks which is a pioneer in Managed Technology Services with over 17+ years of experience in providing end-to-end solutions featuring design, deployment and 24*7 support to top IT companies. We offer world-class managed services for businesses to stay agile & profitable. Our services include 24/7 Network Monitoring, Uptime maintenance, NOC Support, IT Helpdesk services.

    To know about Managed WLAN Services

    ReplyDelete
  3. All your banking hassle, your payments, and receipts are taken care of. It is, in fact, a single-stop solution to all your monetary transactions. One of the two best things about PayPal is its instantaneity. You don’t have to worry about the transaction getting failed, or taking way too much time. Another thing that makes PayPal worthy is its service availability across the world. It follows you wherever you go to make your life easier and quicker. Let’s discuss steps to making an account, and resolutions to PayPal login issues.
    PayPal login |
    www.amazon.com/mytv |
    Cox login |
    DirecTV login |
    Xfinity login |
    youtube.com activate |
    Yahoo Mail Sign

    ReplyDelete
  4. Thanks for sharing informative content randomly landed on your blog but when I go through your blog I feel privileged to read your blog.

    CRM Software in Chennai
    helps distinct sorts of businesses regardless of what their size is. Thus, the customers utilizing this CRM software readily organizes, automates, and enhances their business.

    ReplyDelete
  5. ISC888 สมัคร เพื่อความโปร่งใสในการเดิมพัน ใช้ระบบความปลอดภัยเดียวกับธนาคารทั่วโลก เพื่อยืนยันว่า ข้อมูลของลูกค้าทุกท่านจะปลอดภัยที่สุด สมัคร ISC888 วันนี้ ฟรีเครดิต ลุ้นรับแจ็คพ็อต ทุกวัน.

    ReplyDelete
  6. I loved as much as you will receive carried out right here and, I am really impressed with the many topics information you provide in your article content. Thanks a lot for sharing a piece of wonderful and fantastic information. keep it up and best of luck with your future :) assignment help online - Assignment Provider - auditing assignment

    ReplyDelete
  7. Assignment help in Saudi Arabia allows students to finish their papers on time without having any mistakes. If you want to submit error-free papers in your universities, you must think about Online Assignment help in Saudi Arabia.

    ReplyDelete
  8. Cash App is the easiest way to send, spend, save, and invest your money. It's the SAFE, FAST, and FREE mobile banking app. First of all, you need to install Cash App on your mobile. Tap on the “Sign In” tab. Fill up your login details.
    Cash app login | Cash App Login

    ReplyDelete
  9. Get live news on readerscook
    Breaking news coverage on politics, current affairs, business, sports,technology,lifestyles education, and entertainment.

    ReplyDelete
  10. mywifiext.net is a default web address for Netgear wifi extender setup. If you are unable to access mywifiext setup or www.mywifiext.net login page then our experts can guide you and help you to setup your WiFi range extender.

    Connect your Netgear extender to the router. Run the web browser and visit Netgear default IP 192.168.1.250. You land on the Netgear extender setup webpage. Netgear_ext

    ReplyDelete
  11. Hey admin, My name is Abbie and I am really fan of your skills, I am always searching online for blog content that can help me and y friends. There is obviously a lot to know about this niche info. I think you made some good points in Features also. Keep working, great job essay typer - homework help - Assignment help

    ReplyDelete
  12. Are you searching for assignment help in the UAE? Then don’t worry! We provide you the best assignment writing services at very cheap prices. Visit our website for help with your work.

    ReplyDelete
  13. Hi, I'm Chri mith An Technical Advior. We provide Technical Help to our uer by a diagnoi of their computer and other device. And if there i an iue to be olved, we give out the olution. Thi help the uer to avoid any exiting iue
    AOL Mail
    Roku.com/link
    Roadrunner Email
    TechnicalAdvior

    ReplyDelete
  14. Searching for essay help online in the UK? Then you are at the right place. Our team of professionals is highly experienced in providing online help for essay writing.

    ReplyDelete
  15. Opt for our Assignment Help to finish your assignments and submit them within the deadline. No need to take the stress of insufficient knowledge and lack of skills when you have an online assignment writing expert for writing your assignment in Qatar.

    ReplyDelete
  16. Ready assignments are available just send us message by typing write my assignment for me.

    ReplyDelete

  17. Wonderful blog, here you can get perfect advice regarding Car Transport In Delhi! It Have meaningful and insightful information about the best car transport service like LogisticGuru.PVT. Their associated team members can do every type transport related job, because they are well trained, skilled, and experienced, they can help the customers in their relocation job and make it smooth and damage free.

    ReplyDelete
  18. Why are you getting tense about tech services? I know the best and reliable service for the RR email which will be a good fit for your requirements. I have also used their service many times and I can tell you that they are amazing with their work. Their service is super fast and user friendly. You must visit their Roadrunner email support website.

    Visit their Blog on Roadrunner email problems to get the details.
    Dial our Roadrunner email support number to solve all your Roadrunner email problems.

    Also, if you want help regarding Microsoft office, then visit our Microsoft Office 365 Support website and get to know in detail.

    ReplyDelete
  19. Thanks For Sharing the information.
    If you ever suffer from bad connectivity of your internet connection or have a dead zone network in your home or workplace area. Go with mywifiext setup to solve your internet problem.
    netgear extender setup

    ReplyDelete
  20. We provides a variety of enterprise solutions for network connectivity and managed services that enable large businesses to simplify the complexity of their network in the face of dynamic innovation.
    noc vs soc
    different types of firewalls
    security breach meaning

    ReplyDelete

  21. The students who take Online assignment helpfrom the services do not face any obstacles like limited time or failure of submission or bad marks in writing.



    ReplyDelete
  22. Math was my biggest nightmare for me and my studying was really difficult for me only when I realized that should prepare my math classes 'till I disocver the site where I can order my aacdemic assignments even such as college PowerPoint presentation which my professor asked me to do, especially on math class even which would be difficult for me to cope alone.

    ReplyDelete
  23. Thanks for sharing this unique content. Our Roadrunner email support is a customer care helpline number that is offered by one of the world's best Technical services providers in the USA. To read more about our Roadrunner Email Problems visit our webpage.

    ReplyDelete
  24. if you are looking for online grocery shopping in Durgapur, download Bazaar Durgapur app from playstore, opt for Combo offer to get bigger discount and offers.

    ReplyDelete
  25. There are some of the best platforms from where you can extend the range of your existing wifi network. Linksys extender setup-xxx is one of them, which also provides you the free setup service for your extender. So, to take the benefits, go for it. extender.linksys.com

    ReplyDelete
  26. Thank you for sharing the useful post. A reader got a lot of information from this post and utilized it in their research. I also provide independent support for the outlook email. So if you are facing issues with the outlook account then contact me for outlook support phone number.
    Also Read: Outlook not connecting to server | Outlook send receive error

    ReplyDelete
  27. play cricket online .Instant Paytm Withdrawal Fantasy Power 11 Fantasy Cricket Best App Download Best Fantasy Cricket App in India & win Cash visit Fantasy Cricket Best Website know more Fantasy Cricket Tips. Download Fantasy Power 11 Fantasy Cricket Best App know the Fantasy Cricket Tips and win huge Cash Prizes Fantasy Power 11 Fantasy Cricket Best Website Fantasy Cricket Best App join now & know how to pick a Fantasy Cricket.

    ReplyDelete
  28. The perfect way to get started with Microsoft 365 is gathering enough information and purchasing depending on your requirement. You can then easily download and install the software package by visiting microsoft365.com/setup , microsoft365.com/setup .

    ReplyDelete
  29. The Canon printer that can be downloaded via canon.com/ijsetup page is the best wireless printer that you can connect to your device and print data smoothly. Ij.start canon CD is not the well-suited technique to use ij.start.canon installation for longer. One can canon.com/ijsetup/mg2522 install from another origin if your device is having issues in the online installation or any other.Use ij.start cannon to set up your Canon product.Get started to Canon inkjet setup with guidelines of ij.start.cannonsite.

    ReplyDelete
  30. QuickPay Portal | www.quickpayportal.com | Pay Your Medical Bill

    Pay Your Medical Bill using www.quickpayportal.com and Make a quick and fast payment online using the QuickPay Portal. Just find your QuickPay Code on your billing statement and and you're ready to go


    quickpayportal.com

    quickpayportal.com

    quickpayportal.com

    ReplyDelete
  31. www.kindle.com/support is a platform designed for technical issues related to all Kindle devices. Millions of people around the world have joined Kindle that motivates the Amazon Kindle team to serve best to their readersAmazon Kindle team to serve best to their readers

    ij.start.canon/setup is the easiest way to setup Canon printer to your system. A device and internet connection are basic requirements for making connectivity Canon ij printer setup with computer system or phone.



    How to download and install hp drivers from 123.hp.com/setup? You can download hp assistance to auto update drivers without any hadic



    Go to the Norton Utilities main window and click the how to Install norton install with product key [Antivirus]



    Go to microsoft 365 setup, then log in to your MS account. Next, type in the product key and download the application. Microsoft 365 is the most convenient method to acquire all Office software applications in a single subscription.




    ReplyDelete
  32. Webroot delivers multi-vector protection for endpoints and networks and threat intelligence services to protect businesses and individuals in a connected world.

    ReplyDelete
  33. Garmin Express is a software to manage your Garmin devices from your computer. Ideal for registering your products, but also for synchronizing their data, Garmin Express also allows you to update them.

    ReplyDelete
  34. Webroot SecureanywhereSeptember 2, 2021 at 7:05 AM

    123.hp.com printer setup is used to install and download HP Printer driver software for HP printer setup.

    ReplyDelete
  35. help.microsoft.com talk to a personSeptember 2, 2021 at 7:05 AM

    help.microsoft.com talk to a person will provide you with all the information you need to contact Microsoft Support.

    ReplyDelete
  36. Webroot SecureanywhereSeptember 2, 2021 at 7:08 AM

    Webroot Secureanywhere is world’s leading antivirus software which leads to your system’s sensitive data safety from uncountable cyber threats.

    ReplyDelete
  37. Mcafee Activate is a legendary anti-malware package that doubles as a virus scanner. It comes in handy with a secure firewall, a password manager, real-time VPN, auto-update function, and performance optimizer for total protection.September 2, 2021 at 7:09 AM

    Mcafee Activate is a legendary anti-malware package that doubles as a virus scanner. It comes in handy with a secure firewall, a password manager, real-time VPN, auto-update function, and performance optimizer for total protection.

    ReplyDelete
  38. The Webroot program is highly rated software to protect your devices & data available for download at
    ij.start.canon| ij.start.cannon/ts3322 | Microsoft365.com/setup
    | microsoft365.com/setup

    ReplyDelete
  39. Enter Trend micro activation code on www.trendmciro.com/activate | www.trendmicro/activate to download and activate Trend Micro. To activate Trend micro, make sure you already have an activation code that you’ll probably enter on the trendmicro.com/activate site.

    ReplyDelete
  40. The best way to get online assignment help is to take assistance from GreatAssignmentHelp. We have PhD-level experts working in our team and they write supreme quality assignments for the students.

    ReplyDelete
  41. I love mathematics, but I do not want to do a bachelor's in Mathematics. This is because currently, I am studying economics, and I have a final year dissertation to do now. Therefore, I have to find a professional who will provide economics dissertation writing service at lower rates. This will increase my interest in reading blogs because reading is my all-time favourite hobby.

    ReplyDelete
  42. Such a great post many students need this kind of post please keep writing webroot.com/safe is best Installation Guide.The security package offered by this brand is incredibly easy
    to setup and install. You can easily install and upgrade any of the Webroot Secure Anywhere Antivirus products that help you handle cyber
    security in the best possible manner.

    Download and install or reinstall office setup on a PC or Mac

    garmin.com/express is gps tool
    which enable you to manage your Garmin GPS device from your computer.

    ReplyDelete
  43. very good post keep writing this kind of postij.start.canon/setup is the easiest way to setup Canon printer to your system.
    Steps to connect wired or wireless printer on windows as mac devices are discussed below in this article

    How to download and install hp drivers from 123.hp.com/setup? You can download hp assistance to auto update drivers without any hadic

    If you cannot download or install Norton on your device, read following steps for installing Norton in your PC. Go to the Norton Web link that is norton.com/setup/productkey and then click install button.

    pest control service near me professional not just has the most up to date as well as most effective items,
    however additionally the education and understanding to finish the job right.

    ReplyDelete
  44. Your blog gave us significant data to work with. Each and each tip of your post are amazing. You're the best for sharing. Continue to blog

    ij.start.cannon
    www.office.com/setup
    www.norton.com/setup

    ReplyDelete
  45. Experts can utilize this information to offer flawless programming help. This information is really solution oriented.

    ReplyDelete
  46. Printer in error state” message comes up in a popup box on the desktop screen when the user tries to connect to the device or print from the device. Error codes like this may appear for a variety of reasons, but they are most often caused by a recent software update such as Windows Update that interferes with communication between the system and the attached printer.

    ReplyDelete