Type-checked non-empty strings

https://exploring-better-ways.bellroy.com/haskell-koan-type-checked-non-empty-strings.html

by surprisetalk • 26 days ago

56 49 26 days ago

exploring-better-ways.bellroy.com

Language is not mentioned in a title, so my first thought was about TypeScript type wizardry. Turns out it's as simple as `Exclude<string, "">`.

https://www.typescriptlang.org/docs/handbook/utility-types.h...

Edit: nevermind, LLM fooled me.

ralferoo• 23 days ago

It is very much mentioned in the article title and the first sentence. It's just HN that's truncated the title.

antipurist• 23 days ago

It's simple, and it doesn't work as `Exclude` only applies to union types. For type `string` it just returns the same type `string`.

phpnode• 23 days ago

yup, it's not possible to do it safely with a simple unparameterised type: https://www.typescriptlang.org/play/?#code/C4TwDgpgBAcg9gOwK...

Cthulhu_• 23 days ago

Speaking of TS, there's stuff in there for typing strings / string formats: https://www.typescriptlang.org/docs/handbook/2/template-lite...

nvme0n1p1• 23 days ago

Daily reminder that TypeScript's type checker is not sound.

https://www.typescriptlang.org/play/?#code/C4TwDgpgBAcg9gOwK...

IceDane• 23 days ago

This example is not only wrong for what you intend to demonstrate but even if it wasn't, it's not problematic. In typescript the proper way to do this is using branded types and exporting only the safe constructor, making anyone who wants to violate the invariant go out of their way, which is no different from the situation in any number of programming languages or scenarios.

  declare const brand: unique symbol;
  type NonEmptyString = string & { readonly [brand]: 'NonEmptyString' };

  // the ONLY non-cast way to produce one
  export function nonEmptyString(s: string): NonEmptyString | undefined {
    return s.length > 0 ? (s as NonEmptyString) : undefined;
  }

  export type { NonEmptyString };

blue_pants• 23 days ago

It is true, but it wasn't meant to be sound, so it's okay.

You can do this trick for type-checking emptiness of string literals

https://www.typescriptlang.org/play/?jsx=0#code/C4TwDgpgBAsg...

recursive3• 23 days ago

Daily reminder that the unsoundness in Typescript's type checker is a practical compromise applied to a language that was never designed to be type checked in this way, and furthermore that many developers feel that it strikes a good balance between formal correctness and practical usability.

IshKebab4• 23 days ago

"Huh never heard of Bellroy... I wonder what they're using Haskell for..."

Turns out it's some kind of bags and accessories brand!

qbane• 23 days ago

I pondered for a while, it IS the company I used to know

flexagoon• 23 days ago

I've had a Bellroy bag, they're not the most fashionable but super high quality and well thought-out. Just like Haskell code—maybe that's why they like it.

umpalumpaaa• 23 days ago

In the backpack community bellroy is often seen as “meh”. Eg. they frequently don’t live up to the guarantees they give and to the quality they promise. Also overpriced.

ambicapter• 23 days ago

I once saw a job ad for a company selling a horoscope app that required Haskell. An unusual conjunction for sure.

gib4442• 23 days ago

Using Haskell for a horoscope app is like hiring a mathematician to read tea leaves

saithound5• 23 days ago

Astrology and Haskell are quite similar in that both are much much easier to do if you have a math degree.

_doctor_love9• 23 days ago

An unusual conjunction for sure.

I see what you did there

_jackdk_• 21 days ago

That'd be https://www.costarastrology.com/why-haskell, if I remember the job ad correctly.

kccqzy• 23 days ago

I bought a leather wallet from them in 2016 (the Hide & Seek) and it is still holding up well despite a few loose stitches. It’s much slimmer than my older wallet.

muglug• 23 days ago

Very cool that the language allows specification of a type in this way.

I added a similar type — “non-empty-string” to a typechecker for PHP, and it’s been adopted widely in the PHP ecosystem. It turns out to be pretty handy, especially when there’s a full type system to support it.

gwerbin• 23 days ago

Very cool that the language allows specification of a type in this way.

Check out Idris 2. Dependent types can get very hairy to work with, but that language is an absolute playground for inductive type-level verification. And the standard library is like a nice Haskell standard library to me in a lot of ways, although the language itself is (unsurprisingly) not nearly as "production ready" as Haskell.

VMG2• 23 days ago

Empty strings are usually an artifact of lazy developers paying a minimal "empty" value for a type (just as 0 for numbers).

A type like NonEmptyString is a weak defense against that, as a lazy dev can just pass a single space character or something similar.

anon7000• 23 days ago

But that’s not an empty string

VMG2• 23 days ago

but just as useless

Type-checked non-empty strings

Related Stories