I always thought this kind of thing was abstruse and impractical until I read Type-Driven Development with Idris[0], which made basic dependent type examples--like those demonstrated in the posted article--completely straightforward. Turns out that this kind of thing isn't actually that hard with the right language and tooling.

I highly recommend buying the book and checking out Idris if you found this article interesting. Read the free "overview" chapter[1] at least.

[0] https://www.manning.com/books/type-driven-development-with-i...

[1] https://manning-content.s3.amazonaws.com/download/a/580d6ba-...

This was one of the reasons I felled in love with Turbo Pascal back in the day.

Algol derived languages, while not as powerful as ML ones regarding the type system offer quite a few possibilities to ensure safer code via type definitions, ranges, enumerations and ADTs (Abstract Data Types not to confuse with Algebraic data types).

C++ also allows for this, but requires a bit of boilerplate with templates, classes and operator overloading, which is way more work than a few type declarations in Haskell or Idris.

Yes, this was exactly my feeling reading through the Idris book. In the same way that a few lines of elegant Haskell can sometimes describe functionality that takes all kinds of technically-works-but-only-the-author-understands-it C++ template abuse, a few lines of straightforward Idris can sometimes replace all kinds of Haskell "type family abuse".

all kinds of s can be elegantly described in a few lines of Haskell,

"Type-Driven Development with Idris" is the best Haskell book I've ever read.

With the warning that it's using Idris and strict semantics rather than lazy, I'd almost agree.

I think for Haskell specifically that http://haskellbook.com is the best.

What's the difference in motivation between doing things this way vs with functional dependencies?

Type families are more general than fundeps, and can lead to simpler code with fewer extensions—FunctionalDependencies requires MultiParamTypeClasses, and often FlexibleInstances, FlexibleContexts, and UndecidableInstances.

Fundeps are pretty clear for some simple examples (e.g., a container’s element type is uniquely determined by the container type), but in general I find it easier to think in terms of type-level functions than dependencies between types.

I'm not an experienced Haskell programmer, but I've never seen someone use different names for the type and the type constructor, as in:

    data IntAndChar = MkIntAndChar Int Char

They belong to different namespaces, so you can use the same name:

    data IntAndChar = IntAndChar Int Char

Indeed, I believe this is preferred as it reduces the programmer's cognitive load.

This seems to be the convention in Idris where

  data IntAndChar = IntAndChar Int Char

would not compile with

  Main.IntAndChar already defined.

It's common convention to keep them the same, but in this case it may be useful to distinguish between the type and the term level value.

In this case, I think the different name for the constructor was chosen specifically to show the difference between the term and type level. I think it's a good idea, when explaining Haskell, to not assume that no one gets confused by the constructor and type having the same name (it confused me to begin with).

This article hit the sweet spot for me on so many levels. It's so easy to find very advanced/specialized Haskell tutorials, as well as beginner tutorials, but this stuff -- bridging the two -- is exactly what I was looking for. Please keep these coming, dearest author.

Favorite quote:

> For some reason, functions that operate on types are called type families.

Is there a possibility that length-encoded vectors will be practical someday, or is it just a useful toy example for tutorials?

It depends on how many safety guarantees you want in your code. If you want to be absolutely sure at compile time that eg.. your sort function will not change the number of elements in your list, or you need to be sure that you have read in the expected number of records from a file otherwise you error, then this sort of stuff is practical right now.

Of course you can just stick these checks in your code anyway..

   x = loadstuff
   if x.length == 10 

etc.. but here you are relying on people putting that check in. All functions that have x passed into it then either have to either trust that the loading function made the length check or they have to check the length themselves.

With a stronger type system, you can just put your assumptions into the type system and then if your assumptions are wrong or some code changes to break those assumptions, you will know straight away - even if it is 10 years down the line when junior comes along for his summer holiday work experience and needs to make a change some where...

In Haskell? There are packages like http://hackage.haskell.org/package/vector-sized One might need a typechecker plugin like ghc-typelits-natnormalise http://hackage.haskell.org/package/ghc-typelits-natnormalise to help GHC reason about the lengths.

These two presentations about dependent types in GHC are also good: https://www.youtube.com/watch?v=buVyfrU6QF4 https://www.youtube.com/watch?v=GgD0KUxMaQs

Are people using these packages much in practice? Any pitfalls?

That I don't know.

Basic example: A lot of operations on vectors can be compiled into much more efficient code when the length of the vectors is known at compile time.

Does Haskell/GHC do this in practice, either when using the techniques in the article, or a library like `vector-sized`?

Damn, this is exactly what I was looking for, thanks mate!!!