atacratic

-- I would like to try two options for a bit of code, within the same file...

namespace Option1
    foo : Nat
    bar : Nat -> Nat
    bar n = n + foo

namespace Option2
    foo : Nat
    bar : Nat -> Nat

atacratic

-- idris 1.0
-- idris --noprelude

module Main

infixl 7 <.>

Not : Type -> Type
Not a = a -> Void

atacratic

-- using https://github.com/unisonweb/unison
-- source https://github.com/unisonweb/unison/issues/144

effect Abort where
  Abort : () -> {Abort} a

effect Remote where
  here : {Remote} Node
  transfer : Node -> {Remote} ()

atacratic

Based on Paul and Arya's design here, for a codebase editor for Unison.

Background

Unison functions are content addressed - a function's identity (Id) depends only on its content.

The 'content' here excludes cosmetic stuff that doesn't affect how the function runs, like names, comments and layout.

When one function has a call to another, it refers to it by Id¹.

When I want to talk about a function, I refer to it using a Name. My name for the function might be different from yours though!

atacratic

Comments on https://github.com/unisonweb/unison/blob/8ba5359c8638d5044cd224ef560fc329a1aa0e77/docs/codebase-editor-design.markdown

Core model

• Consider the example of Alice moving the name f from hw3a9 to bww8a, and Bob moving the name f from hw3a9 to 28sja. Am I right that this won't conflict, in this scheme? The two removals agree on hw3a9, and the two additions of the same name on different definitions won't conflict because the MetadataEdits are scoped to a single definition. Doesn't seem right?

• data Codebase = Codebase { code : Set Code, metadata : Map Code (Set Metadata) } You explained that this is for different people to have different metadata for the definition (I think that could do with clarifying in the write-up). I can't quite see how someone would select the Metadata they wanted from the set. How do they know which Set Metadata is theirs / the one they're interested in?

• I'm wondering what happens when two independently discovered versions of a function end up meeti

atacratic

Comments on https://github.com/unisonweb/unison/blob/7fba4e3e091420af79cafd9df5719f0d07a41573/docs/codebase-editor-design.markdown

Seems really good!

There's quite a lot of mathematical structure kicking around in there: Release as the arrows of a category (Namespace as objects); similarly Branch (Namespace' as objects); embedding of Release into Branch; functor from Release down to the monoid that does Namespace -> Namespace composition; similarly from Branch with Namespace' -> Namespace'; Causal as a way of using a Semigroup a to induce a join semilattice on Causal a with some kind of free poset construction... not sure what it all adds up to but it feels rich and interesting.

I really like the way the Branch/Namespace' stuff is an enriched version of Release/Namespace, but with lots of symmetry between the two.

Workflow

atacratic

Here's an unsorted bag of thoughts about the ideas in this draft of Arya's. It's long (sorry) but do see in particular the few bullets at the end.

(1) What's the motivation for going beyond structural types?

If those were all we had, then in the following,

structural Color = Red | Green | Blue | Yellow
warm x = case x of Red -> True; Yellow -> True; _ -> False

structural Direction = North | South | East | West

atacratic

In reply to Arya here...

structural -> nominal

I very much don't want the declared order of the constructors to matter

Let's just talk for now about how we treat code that uses some specific type (rather than about when different types are the same). I think it would be OK for the Unison implementation to remember and use the order (or name) of the constructors to distinguish them, without those things being observable to Unison code. So for example with

structural Decision = Yes | No

...the implementation could use the hash of the original name, or the order of declaration, to record which constructor a function has invoked or which pattern it's matching against. That doesn't itself mean that names or orders are significant in the actual Unison semantics - Unison code has no way of observing it, and the Unison user can't observe it, even by running experiments involving changing names or orders.

atacratic

(Following up the note here.)

Should we even have structural types? What if we just had nominal types only?

In favour of this: less to learn. Having two kinds of type, especially where the difference is so subtle to explain, is a significant spend on our complexity budget.

This idea initially felt surprising, since the structural approach to types is the analogue of how Unison treats terms. But maybe the analogy with terms is misleading. When you're defining a term, it is nothing other than its contents. When you're defining a type, part of what you're doing is constructing an equivalence class of terms, and it's not clear that the id-by-content idea should carry over to that.

What would we lose by dropping structural types?

atacratic

reviewing Unison's LanguageReference.md master@81b65b, i.e. this

Overall:

• This doc is awesome: nicely written, thorough, not trying to be too formal, nice use of examples.
• It needs a table of contents to give the reader an overview.

In ‘type signature’:

• say that Nat means natural number, and that that means whole numbers starting at zero
• ‘meets’->’matches’?