Splitting a string in dhall

Question

I'm playing with dhall and wondered how I can implement a string splitting function of the form

λ(text: Text) -> λ(delimiter: Text) -> List Text

However, it appears dhall has no concept/type to represent individual characters. and there's no such function in the Prelude.

The only thing you can do with Text values is concatenate them

So... is it even possible?

Washery

Answer 1

This is not currently possible with the existing Dhall built-in functions. The Text type is conceptually opaque, similar to Double. The only thing you can do with values of type Text is concatenate them, but you cannot introspect, parse, or compare them for equality.

My original rationale for limiting Text in this way is that the language encourages upstreaming strongly typed representations into its inputs. For example, instead of splitting the string, require that the string has already been split (i.e. expect an input of type List Text instead of Text). However, this could change at some point because the standard is not set in stone and evolves over time through the process outlined here:

• Contributing - How do I change the language?

Also, even without making changes to the language you can still experiment by extending the language with your own built-ins using the Haskell API by following this guide:

• How to add a new built in function

Edit: One thing changed since writing this comment, which is that the language now supports a Text/replace builtin, so even though you still can't split a string you can replace one delimiter with another one. For example:

⊢ Text/replace " " "," "Foo Bar Baz"

"Foo,Bar,Baz"

Asymptotic

How would one process the lines of an input file without a way to split strings? The format of this input file is not up to me to decide, I can’t turn it into a Dhall list. – Continuative

@Ruud: You cannot. String splitting is not possible in Dhall at the time of this writing. – Asymptotic