We're planting a tree for every job application! Click here to learn more

Haskell refactoring and the dependent types

Anton Latukha

23 Dec 2020

2 min read

Haskell refactoring and the dependent types
  • Haskell

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.

Did you like this article?

Anton Latukha

Haskell & Nix & DevOps & telco & math & philosophy. Bio at: https://blog.latukha.com/bio

See other articles by Anton

Related jobs

See all

Title

The company

  • Remote

Title

The company

  • Remote

Title

The company

  • Remote

Title

The company

  • Remote

Related articles

JavaScript Functional Style Made Simple

JavaScript Functional Style Made Simple

Daniel Boros

12 Sep 2021

JavaScript Functional Style Made Simple

JavaScript Functional Style Made Simple

Daniel Boros

12 Sep 2021

WorksHub

CareersCompaniesSitemapFunctional WorksBlockchain WorksJavaScript WorksAI WorksGolang WorksJava WorksPython WorksRemote Works
email iconhello@works-hub.comUK flag

Ground Floor, Verse Building, 18 Brunswick Place, London, N1 6DZ

US flag

108 E 16th Street, New York, NY 10003

Subscribe to our newsletter

Join over 111,000 others and get access to exclusive content, job opportunities and more!

© 2022 WorksHub

Privacy PolicyDeveloped by WorksHub