Introduce 'Never' type as a safe alternative to always None options

Unfortunately, as documented in:

  https://github.com/IntersectMBO/cardano-ledger/issues/4571

  Some Option fields in the script context certificates are going to
  remain set to None, at least until the next Hard fork. There's a risk
  that people permanently lock their funds if they expect deposits on
  registration credentials to ever be `Some`.

  So, we introduce a special type that emulate an `Option` that can only
  ever be `None`. We call it `Never` and it is the first type of this
  kind (i.e. with constructors indexes not starting at 0).
This commit is contained in:
KtorZ
2024-08-27 11:06:02 +02:00
parent ff25fbd970
commit d74e36d0bc
13 changed files with 269 additions and 68 deletions

View File

@@ -0,0 +1,7 @@
# This file was generated by Aiken
# You typically do not need to edit this file
requirements = []
packages = []
[etags]

View File

@@ -0,0 +1,9 @@
name = "aiken-lang/acceptance_test_110"
version = "0.0.0"
license = "Apache-2.0"
description = "Aiken contracts for project 'aiken-lang/110'"
[repository]
user = "aiken-lang"
project = "110"
platform = "github"

View File

@@ -0,0 +1,39 @@
type Foo {
Foo(Int, Never)
Bar
}
test never_is_none() {
let none: Option<Void> = None
trace @"Never": Never
trace @"None": none
let data_never: Data = Never
let data_none: Data = none
data_never == data_none
}
test never_pattern_match() {
when Foo(14, Never) is {
Foo(x, Never) -> x == 14
Bar -> False
}
}
test never_assignment() {
let Never = Never
True
}
test never_wrong_cast() fail {
let data: Data = Some(42)
expect _: Never = data
}
test never_ok_cast() {
let none: Option<Void> = None
let data: Data = none
expect _: Never = data
}