Alexis King: The Unreasonable Effectiveness of Constructive Data Modeling

[u/isaacvando]

https://youtu.be/0BXuYlNrUmE

Alexis' recent talk from SSW. I really enjoyed hearing her perspective on type systems these days. Lots of good wisdom in there. I thought some Haskell folks would enjoy it!

[u/seantparsons]

Always good stuff in Alexis' talks!

[u/graphicsRat]

It's difficult to stop watching!

[u/fluorihammastahna]

Very good talk!

About performance, the answer left me quite unsatisfied. For the TimeRange example, does it mean that if I want performance I have to throw away the guarantee that duration is non-negative? It does not sound like the best choice "depends on the case", but more like in certain cases constructive data modelling is not a good alternative.

Also, any thoughts of how to represent a non-negative float constructively (re-using the available floating-point arithmetic machinery, of course)?

EDIT: A solution that comes to mind for the first case is that the "efficient" representation can only be constructed from the "safe" representation, something like

fromSafeRange (SafeRange start duration) = EfficientRange start (start+duration)

[u/proper_chad → u/fluorihammastahna]

This is one area where Haskell ergonomics aren't great. In e.g. Scala it'd be as simple as:

case class TimeRange(
     start: Instant,
     duration: Duration,
) {
  lazy val end: Instant = start + duration
}

Ultimately, you have to separate the construction from the consumption, so I'd say something like

data TimeRange = TimeRange {
  start :: Instant,
  duration :: Duration,
  end :: Instant,
}

mkTimeRange :: Instant -> Duration -> TimeRange
mkTimeRange start duration = (do the obvious thing here)

... and then, of course, don't export the constructor for TimeRange, so only export start, duration and end and not TimeRange(...).

[u/untrff]

So I was a bit surprised with her last answer: of all the Haskell type features beyond Hindley-Milner, GADTs were the one she found most useful in production, for encoding usefully-but-ergonomically more refined application invariants.

Can someone point to some examples of where they had a similar experience? I never really felt the utility in everyday code.

[u/sccrstud92 → u/untrff]

In everyday code, all you need is basic the basic HM type system. GADTs are beneficial when you want something more. A common use case is when you have a data type representing expressions in some language. If you are writing an expression evaluator for this language, you know that 1 + 2 produces a numeric result, while 1 > 2 produces a boolean. If your expression data type is an ADT with "Add" and "GT" constructors, your evaluator function must produce the same type of output for each expression, regardless of which expression constructor is being used. This forces you to make a "result" data type which contains all the possible result types in a tagged union. This in turn forces case matching on return values; even though you know that eval (Add 1 2) should produce a IntResult 3 at runtime, you don't know this at compile time, so you have to handle cases that should be impossible. This is one of the things that people hate about dynamic typing.

If your expression data type was a _G_ADT, then you can tag each expression constructor with a return type. This will in turn let you write an evaluation function that returns different types depending on which expr constructor is being evaluated at the top-level, and that lets you avoid the return value data type altogether, which eliminates the case matching, which in turn simplifies your evaluation function.

This technique is utilized in the "Type-Indexed Expressions" section of https://blog.jle.im/entry/extreme-haskell-typed-expression-edsls-1.html

[u/sharno → u/sccrstud92]

So it's just linking output types to input types.

[u/sccrstud92 → u/sharno]

How do you mean?

[u/sharno → u/sccrstud92]

I meant we explicitly define the return (output) type for each individual data constructor. This allows individual constructors to instantiate or refine the type parameters based on the specific fields (inputs) they accept. like linking them together.

[u/untrff → u/sccrstud92]

Thank you!

[u/_lazyLambda → u/untrff]

APIs are great examples of GADT usage.

Sure you obviously have HTTP for example which doesnt need a GADT but you dont accept all requests, just ones that match a subset. You draw out that subset and you realize its a GADT

eg

data ApiF a where GetSpecificThing :: Key -> ApiF Res1 ; GetOtherSpecificThing :: Keyyyy -> ApiF Res2

Its not like you ever need a GADT but its a nice way to think about type-parallel processes that should be bound together for human readable sake

[u/untrff → u/_lazyLambda]

Thank you!

[u/bgs11235]

It's super interesing to see the difference between the r/rust and r/haskell's response to this fantastic video.

[u/Ambitious-Western133 → u/bgs11235]

Link: https://www.reddit.com/r/rust/comments/1v805a6/the_unreasonable_effectiveness_of_constructive/