| -- 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 |
| -- idris 1.0 | |
| -- idris --noprelude | |
| module Main | |
| infixl 7 <.> | |
| Not : Type -> Type | |
| Not a = a -> Void |
| -- 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} () |
Based on Paul and Arya's design here, for a codebase editor for Unison.
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 Id1.
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!
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
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.
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.
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
In reply to Arya here...
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.
(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.
Here's a question on using the Unison language.
I wanted to play around with defining APIs for data sources/sinks/feeds etc, but I hit a wall. I don't know how I should define an API in unison without tying down the underlying datatype used to implement it.
As a example, consider the following bit of Haskell.
-- let's ignore for the purposes of this discussion whether this is a wise definition of a stream...
class StreamT s where
get :: s a -> (a, s a)