one type for emptiable and safe non-empty

emptiness-typed

There are many types that promise non-emptiness. One example: MartinSStewart's NonemptyString.

The cool thing is that fromInt, fromChar, etc. keep the compile-time promise of being non-empty, so head, tail, etc. are guaranteed to succeed and you don't have to carry Maybes throughout your program.

How about this: A string type that allows the same operations for non-empty and emptiable values:

toUpper : StringIs canBeEmpty -> StringIs canBeEmpty
length : StringIs canBeEmpty -> Int
...

or even allows passing the (im)possibility of a state from one data structure to another?

toCharList : StringIs canBeEmpty -> ListIs canBeEmpty -- crazy!

All this is very much possible!

Let's try stuff out and see how where we end up:

type StringIs canBeEmpty
    = StringEmpty canBeEmpty
    | StringNotEmpty Char String

fromChar : Char -> StringIs notEmpty_
fromChar onlyChar =
    StringNotEmpty onlyChar ""

head : StringIs Never -> Char
head string =
    case string of
        StringEmpty empty ->
            never empty --! neat
        
        StringNotEmpty headChar _ ->
            headChar

head (char 'E') --> 'E'
head (StringEmpty ()) --> error

the type StringIs Never limits arguments to just StringNotEmpty.

to make the type argument name more descriptive, we could define

type alias NotEmpty =
    Never

Not a good idea:

Html NotEmpty

Next try:

type alias NotEmpty =
    { canBeEmpty : Never }

StringIs.empty
--: StringIs ()

Nice! almost there!

Now let's create toCharList that carries the emptiness-information over:

toCharList : StringIs WAIT -> ListIs HOW_CAN_I_DO_THIS Char

It seems like we need

type alias NotEmpty =
    { canBeEmpty : Never }

StringIs.empty
--: StringIs { canBeEmpty : () }

toCharList :
    StringIs { canBeEmpty : yesOrNever }
    -> ListIs { ... : yesOrNever } Char

CanBe is just a cleaner version of this. It has a simple type tag to make Never values distinct:

type alias NotEmpty =
    CanBe { empty : () } Never

type alias Item =
    CanBe { hole : () } Never

Also, what needed to be written as

type alias Emptiable =
    { canBeEmpty : () }

emptyString : StringIs Emptiable
emptyString =
    StringEmpty { canBeEmpty = () }

becomes simply

emptyString : StringIs (CanBe empty_ ())
emptyString =
    StringEmpty (CanBe ())

Now the fun part:

toCharList :
    StringIs (CanBe emptyString_ yesOrNever) a
    -> ListIs (CanBe emptyList_ yesOrNever) a
toCharList string =
    case string of
        StringEmpty (CanBe yesOrNever) ->
            NothingIs
                --↓ carries over the `yesOrNever` type,
                --↓ while allowing a new tag
                (CanBe yesOrNever)

        StringNotEmpty headChar tailString ->
            ListIs.fromCons headChar (tailString |> String.toList)

the type information gets carried over, so

StringIs.NotEmpty -> ListIs.NotEmpty
CanBe emptyString_ () -> CanBe emptyList_ ()

MaybeIs is just a convenience layer for an optional-able value where a CanBe value is attached to its nothing variant.

type alias StringIs emptyOrNot =
    MaybeIs emptyOrNot ( Char, String )

MaybeIs.map StringIs.head
--: StringIs (CanBe empty_ yesOrNever)
--: -> MaybeIs (CanBe nothing_ yesOrNever) Char

A StringIs acts like a type-safe Maybe NonEmptyString!

Let's create some data structures!

ListIs

Handle Emptiable and NotEmpty lists at once.

MaybeIs emptyOrNot ( a, List b ) is a ListIs emptyOrNot a.

More correctly, it's a ListWithHeadType a emptyOrNot b.

NotEmpty allows safe Maybe-free head, tail, fold (useful for finding the maximum, etc. some call it "fold1"), ...

import ListIs

ListIs.empty         -- ListIs Emptiable a_
    |> ListIs.appendNotEmpty
        (ListIs.fromCons 1 [ 2, 3 ])
                     -- ListIs notEmpty_ Int
    |> ListIs.cons 5 -- ListIs notEmpty_ Int
    |> ListIs.unCons
--> ( 5, [ 1, 2, 3 ] )

HoleyFocusList

A list zipper that can also focus before and after every item.

import HoleyFocusList

HoleyFocusList.empty           -- HoleyFocusList (CanBe hole_ ()) a_
    |> HoleyFocusList.plug 5   -- HoleyFocusList item_ Int
    |> HoleyFocusList.append [ 1, 2, 3 ]
                               -- HoleyFocusList item_ Int
    |> HoleyFocusList.nextHole -- HoleyFocusList (CanBe hole_ ()) Int
    |> HoleyFocusList.toList
--> [ 5, 1, 2, 3 ]

→ zwilias's holey-zipper with a type-safe implementation using MaybeIs and other minor tweaks.

suggestions?

→ See contributing.md

you like type-safety?

typesafe-array takes it to the extreme. The possible length range is part of its type, allowing safe access for some elements.