Skip to content

Instantly share code, notes, and snippets.

@aryairani
Created November 22, 2023 21:14
Show Gist options
  • Save aryairani/c9a3e5f98b0828c2b3aced05b2fe216c to your computer and use it in GitHub Desktop.
Save aryairani/c9a3e5f98b0828c2b3aced05b2fe216c to your computer and use it in GitHub Desktop.
.> builtins.merge

Some basics:

unique type Cat.Dog = Mouse Nat
unique type Rat.Dog = Bird

countCat = cases
  Cat.Dog.Mouse x -> Bird
.> add

Now I want to add a constructor.

unique type Rat.Dog = Bird | Mouse
.> update

Here's the code that update produced:

countCat : Cat.Dog -> Rat.Dog
countCat = cases Mouse x -> Bird

unique type Rat.Dog = Bird | Mouse

Okay, hmm. TBH I think this code should have type-checked without user intervention, but the way it printed (cases Mouse x) is ambiguous, and UCM assumed Mouse meant Rat.Dog.Mouse instead of Cat.Dog.Mouse, which caused parsing to fail.

I'll fix it by making it explicit:

countCat : Cat.Dog -> Rat.Dog
countCat = cases Cat.Dog.Mouse x -> Bird

unique type Rat.Dog = Bird | Mouse

Ok, all set! Now let's update.

.> update

Why is it still printing just Mouse and failing?

Some basics:

unique type Cat.Dog = Mouse Nat
unique type Rat.Dog = Bird

countCat = cases
  Cat.Dog.Mouse x -> Bird
.> add

  ⍟ I've added these definitions:
  
    unique type Cat.Dog
    unique type Rat.Dog
    countCat : Cat.Dog -> Rat.Dog

Now I want to add a constructor.

unique type Rat.Dog = Bird | Mouse
.> update

  Okay, I'm searching the branch for code that needs to be
  updated...

  That's done. Now I'm making sure everything typechecks...

  countCat : Cat.Dog -> Rat.Dog
  countCat = cases Mouse x -> Bird
  
  unique type Rat.Dog = Bird | Mouse

  Typechecking failed. I've updated your scratch file with the
  definitions that need fixing. Once the file is compiling, try
  `update` again.

Here's the code that update produced:

countCat : Cat.Dog -> Rat.Dog
countCat = cases Mouse x -> Bird

unique type Rat.Dog = Bird | Mouse

  This pattern has the wrong number of arguments
  
      2 | countCat = cases Mouse x -> Bird
  
  The constructor has type 
  
    Rat.Dog
  
  but you supplied 1 arguments.

Okay, hmm. TBH I think this code should have type-checked without user intervention, but the way it printed (cases Mouse x) is ambiguous, and UCM assumed Mouse meant Rat.Dog.Mouse instead of Cat.Dog.Mouse, which caused parsing to fail.

I'll fix it by making it explicit:

countCat : Cat.Dog -> Rat.Dog
countCat = cases Cat.Dog.Mouse x -> Bird

unique type Rat.Dog = Bird | Mouse

  I found and typechecked these definitions in scratch.u. If you
  do an `add` or `update`, here's how your codebase would
  change:
  
    ⍟ These names already exist. You can `update` them to your
      new definition:
    
      unique type Rat.Dog
      countCat : Cat.Dog -> Rat.Dog

Ok, all set! Now let's update.

.> update

  Okay, I'm searching the branch for code that needs to be
  updated...

  That's done. Now I'm making sure everything typechecks...

  countCat : Cat.Dog -> Rat.Dog
  countCat = cases Mouse x -> Rat.Dog.Bird
  
  unique type Rat.Dog = Bird | Mouse

  Typechecking failed. I've updated your scratch file with the
  definitions that need fixing. Once the file is compiling, try
  `update` again.

Why is it still ambiguous?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment