mirror of
https://github.com/swarm-game/swarm.git
synced 2024-09-11 14:46:33 +03:00
Add ADT calculator
entity, sum and product type capabilities (#663)
Add `ADT calculator` entity (recipe: `calculator` + `I/O cable` + `typewriter`) which conveys capabilities to work with sum and product types (`inl`, `inr`, `case`; pairs, `fst`, `snd`). Closes #563 .
This commit is contained in:
parent
8366135ae1
commit
12503d114c
@ -722,12 +722,12 @@
|
||||
capabilities: [drill]
|
||||
properties: [portable]
|
||||
|
||||
- name: printer
|
||||
- name: typewriter
|
||||
display:
|
||||
attr: device
|
||||
char: 'Д'
|
||||
description:
|
||||
- A printer is used to inscribe symbols on paper, thus reifying pure, platonic
|
||||
- A typewriter is used to inscribe symbols on paper, thus reifying pure, platonic
|
||||
information into a physical form.
|
||||
properties: [portable]
|
||||
|
||||
@ -908,6 +908,40 @@
|
||||
properties: [portable]
|
||||
capabilities: [arith]
|
||||
|
||||
- name: ADT calculator
|
||||
display:
|
||||
attr: device
|
||||
char: '±'
|
||||
description:
|
||||
- |
|
||||
A calculator with Advanced Display Technology (an attached
|
||||
typewriter that can print out the results). For some reason, in
|
||||
addition to the usual arithmetic on numbers, an ADT calculator can
|
||||
also do arithmetic on types! After all, the helpful typewritten manual
|
||||
explains, a type is just a collection of values, and a finite collection
|
||||
of values is just a fancy number. For example, the type `bool` is
|
||||
just a fancy version of the number 2, where the two things happen to be
|
||||
labelled `false` and `true`.
|
||||
- |
|
||||
The product of two types is a type of pairs, since, for example,
|
||||
if `t` is a type with three elements, then there are 2 * 3 = 6
|
||||
different pairs containing a `bool` and a `t`, that is, 6 elements
|
||||
of type `bool * t`. For working with products of types, the ADT
|
||||
calculator enables pair syntax `(a, b)` as well as the projection
|
||||
functions `fst : a * b -> a` and `snd : a * b -> b`.
|
||||
- |
|
||||
The sum of two types is a type with two options; for example, a
|
||||
value of type `bool + t` is either a `bool` value or a `t` value,
|
||||
and there are 2 + 3 = 5 such values. For working with sums of
|
||||
types, the ADT calculator provides the injection functions `inl :
|
||||
a -> a + b` and `inr : b -> a + b`, as well as the case analysis
|
||||
function `case : (a + b) -> (a -> c) -> (b -> c) -> c`. For
|
||||
example, `case (inl 3) (\x. 2*x) (\y. 3*y) == 6`, and `case (inr
|
||||
3) (\x. 2*x) (\y. 3*y) == 9`.
|
||||
|
||||
properties: [portable]
|
||||
capabilities: [arith, sum, prod]
|
||||
|
||||
- name: compass
|
||||
display:
|
||||
attr: device
|
||||
|
@ -89,7 +89,7 @@
|
||||
- [1, board]
|
||||
- [8, wooden gear]
|
||||
out:
|
||||
- [1, printer]
|
||||
- [1, typewriter]
|
||||
|
||||
#########################################
|
||||
## BITS ##
|
||||
@ -651,6 +651,13 @@
|
||||
out:
|
||||
- [1, calculator]
|
||||
|
||||
- in:
|
||||
- [1, calculator]
|
||||
- [1, typewriter]
|
||||
- [1, I/O cable]
|
||||
out:
|
||||
- [1, ADT calculator]
|
||||
|
||||
- in:
|
||||
- [1, glass]
|
||||
- [1, silver]
|
||||
|
@ -33,6 +33,7 @@ robots:
|
||||
- [1, Tardis]
|
||||
- [1, logger]
|
||||
- [1, solar panel]
|
||||
- [1, ADT calculator]
|
||||
known: [water]
|
||||
world:
|
||||
default: [ice, water]
|
||||
|
@ -116,6 +116,10 @@ data Capability
|
||||
CTime
|
||||
| -- | Capability to execute `try`.
|
||||
CTry
|
||||
| -- | Capability for working with sum types.
|
||||
CSum
|
||||
| -- | Capability for working with product types.
|
||||
CProd
|
||||
| -- | God-like capabilities. For e.g. commands intended only for
|
||||
-- checking challenge mode win conditions, and not for use by
|
||||
-- players.
|
||||
@ -218,6 +222,15 @@ constCaps = \case
|
||||
-- ----------------------------------------------------------------
|
||||
-- exceptions
|
||||
Try -> Just CTry
|
||||
-- ----------------------------------------------------------------
|
||||
-- type-level arithmetic
|
||||
Inl -> Just CSum
|
||||
Inr -> Just CSum
|
||||
Case -> Just CSum
|
||||
Fst -> Just CProd
|
||||
Snd -> Just CProd
|
||||
-- XXX pair syntax should require CProd too
|
||||
|
||||
-- ----------------------------------------------------------------
|
||||
-- Some additional straightforward ones, which however currently
|
||||
-- cannot be used in classic mode since there is no craftable item
|
||||
@ -230,9 +243,4 @@ constCaps = \case
|
||||
-- Some more constants which *ought* to have their own capability but
|
||||
-- currently don't. TODO: #26
|
||||
View -> Nothing -- XXX this should also require something.
|
||||
Inl -> Nothing -- XXX should require cap for sums
|
||||
Inr -> Nothing
|
||||
Case -> Nothing
|
||||
Fst -> Nothing -- XXX should require cap for pairs
|
||||
Snd -> Nothing
|
||||
Knows -> Nothing
|
||||
|
@ -235,7 +235,7 @@ requirements' = go
|
||||
-- the RHS.
|
||||
TBind mx t1 t2 -> go ctx t1 <> go (maybe id Ctx.delete mx ctx) t2
|
||||
-- Everything else is straightforward.
|
||||
TPair t1 t2 -> go ctx t1 <> go ctx t2
|
||||
TPair t1 t2 -> insert (ReqCap CProd) $ go ctx t1 <> go ctx t2
|
||||
TDelay _ t -> go ctx t
|
||||
-- This case should never happen if the term has been
|
||||
-- typechecked; Def commands are only allowed at the top level,
|
||||
|
Loading…
Reference in New Issue
Block a user