Addition of a Void module

[HarrisonGrodin]

Unsure if this is the best format/place for a new proposal (or if I should, say, create a Wiki page). If there's something else I should do, please let me know!

---

Often, it is useful to have access to an empty "void" type. A simple proposal might look like this:

signature VOID =
  sig
    type void
    type t = void
    val absurd : t -> 'a
  end

structure Void :> VOID =
  struct
    datatype void = Void of void
    type t = void
    fun absurd (Void v) = absurd v
  end

Perhaps a few other auxiliary functions could be useful, as well. For example:

    val fail : string -> t  (* raises `Fail` *)
    val asLeft : ('a,t) either -> 'a
    val asRight : (t,'a) either -> 'a

[dmacqueen]

In SML, "Forall t. t" serves the purposes of a void type and is occupied by the single “value” bottom (undefined, nontermination). E.g. fun fail (s: string) = raise Fail s fail : string -> ‘a (fail : (Forall ‘a). string -> ‘a or fail : string -> (Forall ‘a). ‘a) It is not clear to me what additional utility a “void” type would add. Dave MacQueen

On Feb 9, 2021, at 4:40 PM, Harrison Grodin ***@***.***> wrote: Unsure if this is the best format/place for a new proposal (or if I should, say, create a Wiki page). If there's something else I should do, please let me know! Often, it is useful to have access to an empty "void" type. A simple proposal might look like this: signature VOID = sig type void type t = void val absurd : t -> 'a end structure Void :> VOID = struct datatype void = Void of void type t = void fun absurd (Void v) = absurd v end Perhaps a few other auxiliary functions could be useful, as well. For example: val fail : string -> t (* raises `Fail` *) val asLeft : ('a,t) either -> 'a val asRight : (t,'a) either -> 'a — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#31>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAGXNPOQ44XDGEC6FXU4DNDS6HIW7ANCNFSM4XL7STYA>.

David MacQueen [email protected]

[ratmice]

Also discussed in here: SMLFamily/Successor-ML#32

[RobertHarper]

Yes, by that argument, no abstract type is ever needed, you can just hack it up by other means. The point is that void is an abstract type with specified operation, namely absurd aka nullary case.  It ought to be in the Standard Basis. More generally, datatype specifications ought to induce signatures, and nullary datatypes ought to be allowed.  In that case you’d get void “for free” as part of a more general improvement to the language that results from revamping datatypes as modes of use of modules. Bob (c) Robert Harper.  All Rights Reserved.

…

On Feb 14, 2021, 15:56 -0500, David MacQueen ***@***.***>, wrote: In SML, "Forall t. t" serves the purposes of a void type and is occupied by the single “value” bottom (undefined, nontermination). E.g. fun fail (s: string) = raise Fail s fail : string -> ‘a (fail : (Forall ‘a). string -> ‘a or fail : string -> (Forall ‘a). ‘a) It is not clear to me what additional utility a “void” type would add. Dave MacQueen > On Feb 9, 2021, at 4:40 PM, Harrison Grodin ***@***.***> wrote: > > > Unsure if this is the best format/place for a new proposal (or if I should, say, create a Wiki page). If there's something else I should do, please let me know! > > Often, it is useful to have access to an empty "void" type. A simple proposal might look like this: > > signature VOID = > sig > type void > type t = void > val absurd : t -> 'a > end > > structure Void :> VOID = > struct > datatype void = Void of void > type t = void > fun absurd (Void v) = absurd v > end > Perhaps a few other auxiliary functions could be useful, as well. For example: > > val fail : string -> t (* raises `Fail` *) > val asLeft : ('a,t) either -> 'a > val asRight : (t,'a) either -> 'a > — > You are receiving this because you are subscribed to this thread. > Reply to this email directly, view it on GitHub <#31>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAGXNPOQ44XDGEC6FXU4DNDS6HIW7ANCNFSM4XL7STYA>. > David MacQueen ***@***.*** — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or unsubscribe.

[HarrisonGrodin]

While there isn't any particular reason to produce a value of type void as opposed to a new type variable, there are plenty of parameterized datatypes which would benefit from having one parameter set to void. A good example was given in the issue @ratmice mentioned; to add on, void is quite useful in conjunction with recursive types:

datatype 'a term = Var of 'a | Node of string * 'a term list

(* simple example *)
fun traverse (t : void term) : string list =
  case t of
    Var v => absurd v
  | Node (s, children) => s :: List.concatMap traverse children

Here, it's useful to discuss both string terms (terms containing variables) and void terms (ground terms - impossible to have a Var), often at the same time. For example:

val match : string term * void term -> void term StringDict.t

Similarly, with intrinsically-scoped lambda terms, void serves as the empty context:

datatype 'a lam = Var of 'a | App of 'a lam * 'a lam | Lam of 'a option lam

type closed = void lam
val I : closed = Lam (Var NONE)
val K : closed = Lam (Lam (Var (SOME NONE)))
val invalid : closed = Var (raise Fail "impossible")