We use cookies and other tracking technologies to improve your browsing experience on our site, analyze site traffic, and understand where our audience is coming from. To find out more, please read our privacy policy.

By choosing 'I Accept', you consent to our use of cookies and other tracking technologies.

We use cookies and other tracking technologies to improve your browsing experience on our site, analyze site traffic, and understand where our audience is coming from. To find out more, please read our privacy policy.

By choosing 'I Accept', you consent to our use of cookies and other tracking technologies. Less

We use cookies and other tracking technologies... More

Login or register
to apply for this job!

Login or register
to save this job!

Login or register
to save interesting jobs!

Login or register
to get access to all your job applications!

Login or register to start contributing with an article!

Login or register
to see more jobs from this company!

Login or register
to boost this post!

Show some love to the author of this blog by giving their post some rocket fuel 🚀.

Login or register to search for your ideal job!

Login or register to start working on this issue!

Engineers who find a new job through Functional Works average a 15% increase in salary 🚀

Blog hero image

Haskell refactoring and the dependent types

Anton Latukha 20 December, 2020 | 2 min read

Haskell is designed as λ2ω language where terms depend on types: type polymorphism, type classes and families.

Screenshot-2020-12-20-20:06:19.png (image from the Fundamental Haskell book written by me)

It is well-known that Dependently Typed code is not really reusable, because it contradicts with parametric polymorphism. And there is no discussion that it complicates the code, at least it raises the level of complexity of the code and requirements to other programmers, and complicates the type level management/programming especially at times in places where it ties-in with the regular λ2ω type system.

There is a number of extensions, for example, RankNTypes, DataKinds, and others that are really from the λP, λP2 spaces of Lambda Calculus where the types depend on terms.

The terms depend on types and types depend on terms are design contradiction, good design is about what was chosen to use and more importantly what was removed from the language design - good design is not "use everything at once".

"Perfection is achieved, not when there is nothing more to add, but when there is nothing left to take away."

Haskell λ2ω refactoring is easy and great to do. Classical Functional Programming Lisp-style refactoring is a key to good software design, parametric functions can be refactored/simplified into the form that by itself hints to the proper design of the code.

And some practical cases require the use of RankNTypes, DataKinds, and other λP features, and I agree they are areally powerful and sometimes needed.

Adding any λP uses into the code should be only where it is required. Adding the λP properties into the Haskell code makes the code really rigid (difficult to refactoring and extension). Because the main Haskell language and λP directly oppose by design. The reason the CoC is a vast research field - because of its infinite complexity and cases, it is more a mathematical research and proof space than programming space. So to keep the code clean flexible and extensible please try to minimize & localize the λP use and expose the classical λ2ω interfaces from the module. Don't be surprised that because of the λP use and introduced code rigidity, someone would have no other option left during refactoring or feature change but to rewrite the subsystem code all together with its interface, only because the subsystem got rigid by the use of the λP in λ2ω language.

Author's avatar
Anton Latukha
Just a free man, contributing as I can. My almost full bio at: https://blog.latukha.com/bio
    haskell
    Shell
    NIX
    Category Theory
    DevOps
    AWS

Related Issues

cosmos / gaia
  • Open
  • 0
  • 0
  • Intermediate
  • Go
cosmos / gaia
  • Open
  • 0
  • 0
  • Intermediate
  • Go
cosmos / ibc
  • Open
  • 0
  • 0
  • Intermediate
  • TeX
cosmos / ibc
cosmos / ibc
  • Open
  • 0
  • 0
  • Intermediate
  • TeX
WorksHub / client
  • Started
  • 0
  • 28
  • Intermediate
  • Clojure
  • $150
viebel / klipse-clj
viebel / klipse-clj
  • Started
  • 0
  • 4
  • Intermediate
  • Clojure
viebel / klipse
  • Started
  • 0
  • 1
  • Intermediate
  • Clojure
viebel / klipse
  • 1
  • 0
  • Intermediate
  • Clojure

Get hired!

Sign up now and apply for roles at companies that interest you.

Engineers who find a new job through Functional Works average a 15% increase in salary.

Start with GitHubStart with Stack OverflowStart with Email