mirror of
https://github.com/unisonweb/unison.git
synced 2024-08-15 13:30:27 +03:00
updates transcripts
This commit is contained in:
parent
51e2ea0898
commit
79ad0fa8df
@ -10,8 +10,8 @@ Let's set up some definitions to start:
|
||||
x = 1
|
||||
y = 2
|
||||
|
||||
type X = One Nat
|
||||
type Y = Two Nat Nat
|
||||
structural type X = One Nat
|
||||
structural type Y = Two Nat Nat
|
||||
```
|
||||
|
||||
Expected: `x` and `y`, `X`, and `Y` exist as above. UCM tells you this.
|
||||
@ -25,7 +25,7 @@ Let's add an alias for `1` and `One`:
|
||||
```unison
|
||||
z = 1
|
||||
|
||||
type Z = One Nat
|
||||
structural type Z = One Nat
|
||||
```
|
||||
|
||||
Expected: `z` is now `1`. UCM tells you that this definition is also called `x`.
|
||||
@ -39,7 +39,7 @@ Let's update something that has an alias (to a value that doesn't have a name al
|
||||
|
||||
```unison
|
||||
x = 3
|
||||
type X = Three Nat Nat Nat
|
||||
structural type X = Three Nat Nat Nat
|
||||
```
|
||||
|
||||
Expected: `x` is now `3` and `X` has constructor `Three`. UCM tells you the old definitions were also called `z` and `Z` and these names have also been updated.
|
||||
@ -52,7 +52,7 @@ Update it to something that already exists with a different name:
|
||||
|
||||
```unison
|
||||
x = 2
|
||||
type X = Two Nat Nat
|
||||
structural type X = Two Nat Nat
|
||||
```
|
||||
|
||||
Expected: `x` is now `2` and `X` is `Two`. UCM says the old definition was also named `z/Z`, and was also updated. And it says the new definition is also named `y/Y`.
|
||||
|
@ -6,8 +6,8 @@ Let's set up some definitions to start:
|
||||
x = 1
|
||||
y = 2
|
||||
|
||||
type X = One Nat
|
||||
type Y = Two Nat Nat
|
||||
structural type X = One Nat
|
||||
structural type Y = Two Nat Nat
|
||||
```
|
||||
|
||||
```ucm
|
||||
@ -18,8 +18,8 @@ type Y = Two Nat Nat
|
||||
|
||||
⍟ These new definitions are ok to `add`:
|
||||
|
||||
type X
|
||||
type Y
|
||||
structural type X
|
||||
structural type Y
|
||||
x : Nat
|
||||
y : Nat
|
||||
|
||||
@ -33,8 +33,8 @@ Expected: `x` and `y`, `X`, and `Y` exist as above. UCM tells you this.
|
||||
|
||||
⍟ I've added these definitions:
|
||||
|
||||
type X
|
||||
type Y
|
||||
structural type X
|
||||
structural type Y
|
||||
x : Nat
|
||||
y : Nat
|
||||
|
||||
@ -44,7 +44,7 @@ Let's add an alias for `1` and `One`:
|
||||
```unison
|
||||
z = 1
|
||||
|
||||
type Z = One Nat
|
||||
structural type Z = One Nat
|
||||
```
|
||||
|
||||
```ucm
|
||||
@ -55,7 +55,7 @@ type Z = One Nat
|
||||
|
||||
⍟ These new definitions are ok to `add`:
|
||||
|
||||
type Z
|
||||
structural type Z
|
||||
(also named X)
|
||||
z : Nat
|
||||
(also named x)
|
||||
@ -69,7 +69,7 @@ Also, `Z` is an alias for `X`.
|
||||
|
||||
⍟ I've added these definitions:
|
||||
|
||||
type Z
|
||||
structural type Z
|
||||
(also named X)
|
||||
z : Nat
|
||||
(also named x)
|
||||
@ -79,7 +79,7 @@ Let's update something that has an alias (to a value that doesn't have a name al
|
||||
|
||||
```unison
|
||||
x = 3
|
||||
type X = Three Nat Nat Nat
|
||||
structural type X = Three Nat Nat Nat
|
||||
```
|
||||
|
||||
```ucm
|
||||
@ -91,7 +91,7 @@ type X = Three Nat Nat Nat
|
||||
⍟ These names already exist. You can `update` them to your
|
||||
new definition:
|
||||
|
||||
type X
|
||||
structural type X
|
||||
(The old definition is also named Z. I'll update this
|
||||
name too.)
|
||||
x : Nat
|
||||
@ -106,7 +106,7 @@ Expected: `x` is now `3` and `X` has constructor `Three`. UCM tells you the old
|
||||
|
||||
⍟ I've updated these names to your new definition:
|
||||
|
||||
type X
|
||||
structural type X
|
||||
(The old definition was also named Z. I updated this name
|
||||
too.)
|
||||
x : Nat
|
||||
@ -118,7 +118,7 @@ Update it to something that already exists with a different name:
|
||||
|
||||
```unison
|
||||
x = 2
|
||||
type X = Two Nat Nat
|
||||
structural type X = Two Nat Nat
|
||||
```
|
||||
|
||||
```ucm
|
||||
@ -130,7 +130,7 @@ type X = Two Nat Nat
|
||||
⍟ These names already exist. You can `update` them to your
|
||||
new definition:
|
||||
|
||||
type X
|
||||
structural type X
|
||||
(The old definition is also named Z. I'll update this
|
||||
name too.)
|
||||
(The new definition is already named Y as well.)
|
||||
@ -147,7 +147,7 @@ Expected: `x` is now `2` and `X` is `Two`. UCM says the old definition was also
|
||||
|
||||
⍟ I've updated these names to your new definition:
|
||||
|
||||
type X
|
||||
structural type X
|
||||
(The old definition was also named Z. I updated this name
|
||||
too.)
|
||||
(The new definition is already named Y as well.)
|
||||
|
@ -87,10 +87,10 @@ Let's try it!
|
||||
64. Doc.Link : Link -> Doc
|
||||
65. Doc.Signature : Term -> Doc
|
||||
66. Doc.Source : Link -> Doc
|
||||
67. type Either a b
|
||||
67. structural type Either a b
|
||||
68. Either.Left : a -> Either a b
|
||||
69. Either.Right : b -> Either a b
|
||||
70. ability Exception
|
||||
70. structural ability Exception
|
||||
71. Exception.raise : Failure ->{Exception} x
|
||||
72. builtin type Float
|
||||
73. Float.* : Float -> Float -> Float
|
||||
@ -402,11 +402,11 @@ Let's try it!
|
||||
312. Nat.toText : Nat -> Text
|
||||
313. Nat.trailingZeros : Nat -> Nat
|
||||
314. Nat.xor : Nat -> Nat -> Nat
|
||||
315. type Optional a
|
||||
315. structural type Optional a
|
||||
316. Optional.None : Optional a
|
||||
317. Optional.Some : a -> Optional a
|
||||
318. builtin type Request
|
||||
319. type SeqView a b
|
||||
319. structural type SeqView a b
|
||||
320. SeqView.VElem : a -> b -> SeqView a b
|
||||
321. SeqView.VEmpty : SeqView a b
|
||||
322. unique type Test.Result
|
||||
@ -432,9 +432,9 @@ Let's try it!
|
||||
342. Text.uncons : Text -> Optional (Char, Text)
|
||||
343. Text.unsnoc : Text -> Optional (Text, Char)
|
||||
344. todo : a -> b
|
||||
345. type Tuple a b
|
||||
345. structural type Tuple a b
|
||||
346. Tuple.Cons : a -> b -> Tuple a b
|
||||
347. type Unit
|
||||
347. structural type Unit
|
||||
348. Unit.Unit : ()
|
||||
349. Universal.< : a -> a -> Boolean
|
||||
350. Universal.<= : a -> a -> Boolean
|
||||
|
@ -10,8 +10,8 @@ Let's set up some definitions to start:
|
||||
x = 1
|
||||
y = 2
|
||||
|
||||
type X = One Nat
|
||||
type Y = Two Nat Nat
|
||||
structural type X = One Nat
|
||||
structural type Y = Two Nat Nat
|
||||
```
|
||||
|
||||
```ucm
|
||||
|
@ -18,7 +18,7 @@ unambiguous type.
|
||||
|
||||
```unison:hide
|
||||
foo = 1
|
||||
type Foo = Foo Nat
|
||||
structural type Foo = Foo Nat
|
||||
```
|
||||
|
||||
```ucm
|
||||
@ -60,7 +60,7 @@ A delete should remove both versions of the term.
|
||||
Let's repeat all that on a type, for completeness.
|
||||
|
||||
```unison:hide
|
||||
type Foo = Foo Nat
|
||||
structural type Foo = Foo Nat
|
||||
```
|
||||
|
||||
```ucm
|
||||
@ -68,7 +68,7 @@ type Foo = Foo Nat
|
||||
```
|
||||
|
||||
```unison:hide
|
||||
type Foo = Foo Boolean
|
||||
structural type Foo = Foo Boolean
|
||||
```
|
||||
|
||||
```ucm
|
||||
@ -88,7 +88,7 @@ Finally, let's try to delete a term and a type with the same name.
|
||||
|
||||
```unison:hide
|
||||
foo = 1
|
||||
type foo = Foo Nat
|
||||
structural type foo = Foo Nat
|
||||
```
|
||||
|
||||
```ucm
|
||||
|
@ -18,7 +18,7 @@ unambiguous type.
|
||||
|
||||
```unison
|
||||
foo = 1
|
||||
type Foo = Foo Nat
|
||||
structural type Foo = Foo Nat
|
||||
```
|
||||
|
||||
```ucm
|
||||
@ -26,7 +26,7 @@ type Foo = Foo Nat
|
||||
|
||||
⍟ I've added these definitions:
|
||||
|
||||
type Foo
|
||||
structural type Foo
|
||||
foo : Nat
|
||||
|
||||
.> delete foo
|
||||
@ -41,7 +41,7 @@ type Foo = Foo Nat
|
||||
|
||||
Removed definitions:
|
||||
|
||||
1. type Foo
|
||||
1. structural type Foo
|
||||
|
||||
Tip: You can use `undo` or `reflog` to undo this change.
|
||||
|
||||
@ -128,7 +128,7 @@ A delete should remove both versions of the term.
|
||||
Let's repeat all that on a type, for completeness.
|
||||
|
||||
```unison
|
||||
type Foo = Foo Nat
|
||||
structural type Foo = Foo Nat
|
||||
```
|
||||
|
||||
```ucm
|
||||
@ -136,11 +136,11 @@ type Foo = Foo Nat
|
||||
|
||||
⍟ I've added these definitions:
|
||||
|
||||
type Foo
|
||||
structural type Foo
|
||||
|
||||
```
|
||||
```unison
|
||||
type Foo = Foo Boolean
|
||||
structural type Foo = Foo Boolean
|
||||
```
|
||||
|
||||
```ucm
|
||||
@ -148,7 +148,7 @@ type Foo = Foo Boolean
|
||||
|
||||
⍟ I've added these definitions:
|
||||
|
||||
type Foo
|
||||
structural type Foo
|
||||
|
||||
.a> merge .b
|
||||
|
||||
@ -157,12 +157,12 @@ type Foo = Foo Boolean
|
||||
|
||||
New name conflicts:
|
||||
|
||||
1. type Foo#d97e0jhkmd
|
||||
1. structural type Foo#d97e0jhkmd
|
||||
|
||||
↓
|
||||
2. ┌ type Foo#d97e0jhkmd
|
||||
2. ┌ structural type Foo#d97e0jhkmd
|
||||
|
||||
3. └ type Foo#gq9inhvg9h
|
||||
3. └ structural type Foo#gq9inhvg9h
|
||||
|
||||
|
||||
4. Foo.Foo#d97e0jhkmd#0 : Nat -> Foo#d97e0jhkmd
|
||||
@ -181,7 +181,7 @@ type Foo = Foo Boolean
|
||||
|
||||
Removed definitions:
|
||||
|
||||
1. type a.Foo#d97e0jhkmd
|
||||
1. structural type a.Foo#d97e0jhkmd
|
||||
|
||||
Name changes:
|
||||
|
||||
@ -212,7 +212,7 @@ Finally, let's try to delete a term and a type with the same name.
|
||||
|
||||
```unison
|
||||
foo = 1
|
||||
type foo = Foo Nat
|
||||
structural type foo = Foo Nat
|
||||
```
|
||||
|
||||
```ucm
|
||||
@ -220,7 +220,7 @@ type foo = Foo Nat
|
||||
|
||||
⍟ I've added these definitions:
|
||||
|
||||
type foo
|
||||
structural type foo
|
||||
foo : Nat
|
||||
|
||||
```
|
||||
@ -229,7 +229,7 @@ type foo = Foo Nat
|
||||
|
||||
Removed definitions:
|
||||
|
||||
1. type foo
|
||||
1. structural type foo
|
||||
2. foo : Nat
|
||||
|
||||
Tip: You can use `undo` or `reflog` to undo this change.
|
||||
|
@ -7,12 +7,12 @@ I can use `debug.file` to see the hashes of the last typechecked file.
|
||||
|
||||
Given this .u file:
|
||||
```unison:hide
|
||||
type outside.A = A Nat outside.B
|
||||
type outside.B = B Int
|
||||
structural type outside.A = A Nat outside.B
|
||||
structural type outside.B = B Int
|
||||
outside.c = 3
|
||||
outside.d = c < (p + 1)
|
||||
|
||||
type inside.M = M outside.A
|
||||
structural type inside.M = M outside.A
|
||||
inside.p = c
|
||||
inside.q x = x + p * p
|
||||
inside.r = d
|
||||
@ -35,4 +35,4 @@ But wait, there's more. I can check the dependencies and dependents of a defini
|
||||
.>
|
||||
```
|
||||
|
||||
We don't have an index for dependents of constructors, but iirc if you ask for that, it will show you dependents of the type that provided the constructor.
|
||||
We don't have an index for dependents of constructors, but iirc if you ask for that, it will show you dependents of the structural type that provided the constructor.
|
||||
|
@ -3,12 +3,12 @@ I can use `debug.file` to see the hashes of the last typechecked file.
|
||||
|
||||
Given this .u file:
|
||||
```unison
|
||||
type outside.A = A Nat outside.B
|
||||
type outside.B = B Int
|
||||
structural type outside.A = A Nat outside.B
|
||||
structural type outside.B = B Int
|
||||
outside.c = 3
|
||||
outside.d = c < (p + 1)
|
||||
|
||||
type inside.M = M outside.A
|
||||
structural type inside.M = M outside.A
|
||||
inside.p = c
|
||||
inside.q x = x + p * p
|
||||
inside.r = d
|
||||
@ -36,9 +36,9 @@ But wait, there's more. I can check the dependencies and dependents of a defini
|
||||
|
||||
⍟ I've added these definitions:
|
||||
|
||||
type inside.M
|
||||
type outside.A
|
||||
type outside.B
|
||||
structural type inside.M
|
||||
structural type outside.A
|
||||
structural type outside.B
|
||||
inside.p : Nat
|
||||
inside.q : Nat -> Nat
|
||||
inside.r : Boolean
|
||||
@ -90,4 +90,4 @@ But wait, there's more. I can check the dependencies and dependents of a defini
|
||||
1. #im2kiu2hmn inside.r
|
||||
|
||||
```
|
||||
We don't have an index for dependents of constructors, but iirc if you ask for that, it will show you dependents of the type that provided the constructor.
|
||||
We don't have an index for dependents of constructors, but iirc if you ask for that, it will show you dependents of the structural type that provided the constructor.
|
||||
|
@ -10,7 +10,7 @@ Unison documentation is written in Unison. Documentation is a value of the follo
|
||||
.> view builtin.Doc
|
||||
```
|
||||
|
||||
You can create these `Doc` values with ordinary code, or you can use the special syntax. A value of type `Doc` can be created via syntax like:
|
||||
You can create these `Doc` values with ordinary code, or you can use the special syntax. A value of structural type `Doc` can be created via syntax like:
|
||||
|
||||
```unison
|
||||
use .builtin
|
||||
|
@ -76,9 +76,9 @@ baz bar = (bar, 42) -- here, `bar` refers to the parameter
|
||||
This should also typecheck, using the local `Sun`, and not `Day.Sun` which exists in the codebase, and the local `Day`, not the codebase `Day`.
|
||||
|
||||
```unison:hide
|
||||
type Zoot = Zonk | Sun
|
||||
structural type Zoot = Zonk | Sun
|
||||
|
||||
type Day = Day Int
|
||||
structural type Day = Day Int
|
||||
|
||||
use Zoot Zonk
|
||||
|
||||
@ -96,7 +96,7 @@ day1 = Day +1
|
||||
Even though local definitions are preferred, you can refer to definitions in the codebase via any unique suffix that doesn't also exist in the file.
|
||||
|
||||
```unison:hide
|
||||
type Zoot = Zonk | Sun
|
||||
structural type Zoot = Zonk | Sun
|
||||
|
||||
use Zoot Zonk
|
||||
|
||||
|
@ -68,9 +68,9 @@ baz bar = (bar, 42) -- here, `bar` refers to the parameter
|
||||
This should also typecheck, using the local `Sun`, and not `Day.Sun` which exists in the codebase, and the local `Day`, not the codebase `Day`.
|
||||
|
||||
```unison
|
||||
type Zoot = Zonk | Sun
|
||||
structural type Zoot = Zonk | Sun
|
||||
|
||||
type Day = Day Int
|
||||
structural type Day = Day Int
|
||||
|
||||
use Zoot Zonk
|
||||
|
||||
@ -88,7 +88,7 @@ day1 = Day +1
|
||||
Even though local definitions are preferred, you can refer to definitions in the codebase via any unique suffix that doesn't also exist in the file.
|
||||
|
||||
```unison
|
||||
type Zoot = Zonk | Sun
|
||||
structural type Zoot = Zonk | Sun
|
||||
|
||||
use Zoot Zonk
|
||||
|
||||
|
@ -19,9 +19,13 @@ dialog = Ask.provide 'zoot '("Awesome number: " ++ Nat.toText Ask.ask ++ "!")
|
||||
|
||||
```ucm
|
||||
|
||||
The expression in red needs the {Zoot} ability, but this location does not have access to any abilities.
|
||||
I expected to see `structural` or `unique` at the start of
|
||||
this line:
|
||||
|
||||
13 | dialog = Ask.provide 'zoot '("Awesome number: " ++ Nat.toText Ask.ask ++ "!")
|
||||
1 | ability Ask where ask : Nat
|
||||
|
||||
Learn more about when to use `structural` vs `unique` in the
|
||||
Unison Docs:
|
||||
https://www.unisonweb.org/docs/language-reference/#unique-types
|
||||
|
||||
```
|
||||
|
@ -1,6 +1,6 @@
|
||||
|
||||
```unison
|
||||
type One a = One a
|
||||
structural type One a = One a
|
||||
unique type Woot a b c = Woot a b c
|
||||
unique type Z = Z
|
||||
|
||||
|
@ -1,6 +1,6 @@
|
||||
|
||||
```unison
|
||||
type One a = One a
|
||||
structural type One a = One a
|
||||
unique type Woot a b c = Woot a b c
|
||||
unique type Z = Z
|
||||
|
||||
@ -18,7 +18,7 @@ snoc k aN = match k with
|
||||
|
||||
⍟ These new definitions are ok to `add`:
|
||||
|
||||
type One a
|
||||
structural type One a
|
||||
unique type Woot a b c
|
||||
unique type Z
|
||||
snoc : One a -> aN -> Woot (One a) (One aN) ##Nat
|
||||
|
@ -12,7 +12,7 @@ ability'' = 90
|
||||
-- this type is the same as `type Either a b = Left a | Right b`
|
||||
-- but with very confusing names
|
||||
-- seriously don't ever do this
|
||||
type type! type_ ability_ = ability' type_ | type! type_
|
||||
structural type type! type_ ability_ = ability' type_ | type! type_
|
||||
|
||||
unique type type!!! type_ ability_ = ability' type_ | type! type_
|
||||
```
|
||||
|
@ -12,7 +12,7 @@ ability'' = 90
|
||||
-- this type is the same as `type Either a b = Left a | Right b`
|
||||
-- but with very confusing names
|
||||
-- seriously don't ever do this
|
||||
type type! type_ ability_ = ability' type_ | type! type_
|
||||
structural type type! type_ ability_ = ability' type_ | type! type_
|
||||
|
||||
unique type type!!! type_ ability_ = ability' type_ | type! type_
|
||||
```
|
||||
@ -25,7 +25,7 @@ unique type type!!! type_ ability_ = ability' type_ | type! type_
|
||||
|
||||
⍟ These new definitions are ok to `add`:
|
||||
|
||||
type type! type_ ability_
|
||||
structural type type! type_ ability_
|
||||
unique type type!!! type_ ability_
|
||||
ability! : ##Nat
|
||||
ability'' : ##Nat
|
||||
|
@ -12,7 +12,7 @@ unique type A a b c d
|
||||
| C c
|
||||
| D d
|
||||
|
||||
type NeedsA a b = NeedsA (A a b Nat Nat)
|
||||
structural type NeedsA a b = NeedsA (A a b Nat Nat)
|
||||
| Zoink Text
|
||||
|
||||
f : A Nat Nat Nat Nat -> Nat
|
||||
@ -66,7 +66,7 @@ Let's do the update now, and verify that the definitions all look good and there
|
||||
Here's a test of updating a record:
|
||||
|
||||
```unison
|
||||
type Rec = { uno : Nat, dos : Nat }
|
||||
structural type Rec = { uno : Nat, dos : Nat }
|
||||
|
||||
combine r = uno r + dos r
|
||||
```
|
||||
@ -76,7 +76,7 @@ combine r = uno r + dos r
|
||||
```
|
||||
|
||||
```unison
|
||||
type Rec = { uno : Nat, dos : Nat, tres : Text }
|
||||
structural type Rec = { uno : Nat, dos : Nat, tres : Text }
|
||||
```
|
||||
|
||||
And checking that after updating this record, there's nothing `todo`:
|
||||
|
@ -73,7 +73,7 @@ it again shows the definition using the multi-argument `cases` syntax opportunis
|
||||
Here's another example:
|
||||
|
||||
```unison
|
||||
type B = T | F
|
||||
structural type B = T | F
|
||||
|
||||
blah = cases
|
||||
T, x -> "hi"
|
||||
|
@ -117,7 +117,7 @@ it again shows the definition using the multi-argument `cases` syntax opportunis
|
||||
Here's another example:
|
||||
|
||||
```unison
|
||||
type B = T | F
|
||||
structural type B = T | F
|
||||
|
||||
blah = cases
|
||||
T, x -> "hi"
|
||||
@ -140,7 +140,7 @@ blorf = cases
|
||||
|
||||
⍟ These new definitions are ok to `add`:
|
||||
|
||||
type B
|
||||
structural type B
|
||||
blah : B -> B -> Text
|
||||
blorf : B -> B -> B
|
||||
|
||||
|
@ -4,7 +4,7 @@
|
||||
```
|
||||
|
||||
```unison:hide
|
||||
type IntTriple = IntTriple (Int, Int, Int)
|
||||
structural type IntTriple = IntTriple (Int, Int, Int)
|
||||
intTriple = IntTriple(+1, +1, +1)
|
||||
```
|
||||
|
||||
|
@ -1,6 +1,6 @@
|
||||
Example uses of the `names` command and output
|
||||
```unison
|
||||
type IntTriple = IntTriple (Int, Int, Int)
|
||||
structural type IntTriple = IntTriple (Int, Int, Int)
|
||||
intTriple = IntTriple(+1, +1, +1)
|
||||
```
|
||||
|
||||
|
@ -6,7 +6,7 @@ FYI, here are the `Exception` and `Failure` types:
|
||||
```ucm
|
||||
.> view Exception Failure
|
||||
|
||||
ability builtin.Exception where
|
||||
structural ability builtin.Exception where
|
||||
raise : Failure ->{builtin.Exception} x
|
||||
|
||||
unique type builtin.io2.Failure
|
||||
|
Loading…
Reference in New Issue
Block a user