How to type Erlang terms without built-in types.

[lpil]

Hello!

I wish to add a set module to alpaca_lib. Given the term is defined in Erlang and not Alpaca how do I define the type?

I could do something like type set 'a = Set but then I have this Set constructor that can be incorrectly used in place of an actual set term.

Is something like beam_type Set needed? Or perhaps we could have type set without an = ... for this.

[j14159]

Great question/point, thanks! I've had some related thoughts around a kind of opaque/foreign type, e.g. for saying "this value coming back is type x and Alpaca code can't inspect it, just pass it back out via FFI, etc".

Full disclosure: I may be using the term "opaque type" incorrectly but I do think what we're talking about is information hiding to some degree?

Would something like the following work do you think?

module sets
 
opaque type set 'a

val addElement 'a : fn 'a (set 'a) -> (set 'a)
let addElement e s =
  beam :sets :add_element [e, s] with
    | s2 -> s2

I think if we have something like opaque types they would have to be disallowed in unqualified unions, e.g. type t = set 'a | int has to be a type error.

Thoughts?

EDIT: I used snake case, corrected to camel :( Old habits!

[lpil]

Sounds sensible to me, though I could see some unions needing qualification and some not being confusing.

[j14159]

I could see some unions needing qualification and some not being confusing

I think it's more an issue for the type inferencer than anything else to be honest.

Some details, given:

opaque type set 'a
type t = int | set 'a

Then here:

let foo x = match x with
  | i, isInteger i -> "got an integer"
  | s              -> "got a set"

The typer actually has no way to know that s is a set 'a (no evidence for it) so it would reasonably fail since:

• we might actually want something other than t and have forgotten to define or import it. Defaulting to t may be more confusing than not to the user.
• we can't define a valid Erlang guard function for sets:is_set (though we could fake it by generating at least one more nested match expression transparently to the user perhaps).
• adding a type spec doesn't bypass the inferencer. The inferencer runs on the function first and then if the function's type and spec unify (meaning if the spec is at least as specific as the inferred type), we use the spec's type.

In this case things should be unambiguous for the typer:

opaque type set 'a
type t = int | Set set 'a

let foo x = match x with
  | i, isInteger i -> "got an integer"
  | Set s          -> "got a set"

(I think we could even drop the isInteger guard)
But a "decidability switch" would force us to do this:

opaque type set 'a
type t = Int int | Set set 'a

let foo x = match x with
  | Int i -> "got an integer"
  | Set s -> "got a set"

(ignoring issues with decidability of record types that I've been reading hints of in 1ML papers but do not yet understand)

[lpil]

opaque type set 'a
type t = Int int | Set set 'a

let foo x = match x with
  | Int i -> "got an integer"
  | Set s -> "got a set"

This example where both are qualified looks like the clearest approach to me (perhaps because I'm used to Haskell and Elm).

It would be my preference for there to be as few extra rules to remember in the language, especially if the rules are based around implementation details of the language.

[j14159]

It would be my preference for there to be as few extra rules to remember in the language

I tend to agree. Unqualified vs qualified (or untagged vs tagged) have come up a few times in conversation with both @danabr and @lepoetemaudit over the last year or so. Unions without constructors were consciously made part of Alpaca initially because Erlang programs could quite easily send a mix of types without constructors and I thought it might be best to support this. I'm less and less sure as time goes by :)

One thing that might be more reasonable is to require constructors with a per-module switch to degrade the type system, allowing untagged unions in special cases for Erlang interop. I'm not 100% sure yet but I think "decidable by default, understand the rules if you want to play with fire" might be the better direction.

[lpil]

Another alternative could be a system like Purescripts Foreign and Elm's Json, where from FFI we get an opaque foreign value that we have to explicitly attempt to decode with functions such as

val decodeInt : fn foreignData -> result string int

This can get boilerplate-y though. In Elm I write a lot of decoders that look like this:

decoder : Decoder VideoLibraryItem
decoder =
    decode VideoLibraryItem
        |> required "id" int
        |> required "title" string
        |> required "created_at" date
        |> optional "placer_name" (nullable string) Nothing

and are run with

decodeValue : Decoder a -> Value -> Result String a

A "trust me, I know what I'm doing" escape hatch would likely be required though for places where this overhead is impractical. i.e. implementing alpaca_lib

[j14159]

I think we're now moving a little into the realm of #7 here but that's probably a good thing.

I'm not super keen on an unqualified "trust me" but a "trust me but check for me and explode if I got it wrong" I think is arguably helpful. For something like this we'd need to add guards and recursive checks at the code gen stage so there would be a performance penalty but might be worthwhile sometimes?