Prevent invalid input with dependent types - a fixed solution - 2021-11-02

Guillaume Allais highlighted for the previous post, that the pattern function allows the caller to specify other value for the parsed implicit parameter by overriding the default value.

So it is possible to call pattern with a route pattern string "/*" and pass in a ParsedPattern "/other" parameter, which would result in an inconsistent behaviour.

Prevent invalid input with dependent types - 2021-10-31

As an application developer I’ve always wanted to enhance developer experience. The most common tool for this is a statically typed programming language. It is fascinating what such programming languages can do in compile time, and what amount of issues they can prevent at runtime.

However most of these languages are limited to their own language domains, they require external tools or plugins to extend their capabilities. In this post I would like to show you a simple problem in the server side web development domain, which can be solved with dependent types in idris programming language.