tweag/nickel
1
1
Fork 0
mirror of https://github.com/tweag/nickel.git synced 2024-10-03 22:57:11 +03:00
Code Issues Projects Releases Wiki Activity

Fix typo in notes/sum-as-dependent-records.md

Browse Source
This commit is contained in:
Yann Hamdaoui 2022-01-12 13:48:49 +01:00 committed by GitHub
parent cce3b6c4b0
commit aa2958c6fa
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
notes/sum-as-dependent-records.md
View File

@ -9,7 +9,7 @@ The idea would be to encode sums by using Pi and Sigma types: `A+B` would become
For this, we'd need to implement two new kind of contracts:
* Dependent functions, `x: A -> \x. B`, which allow the codomain contract to depend on the input, as a reference we have [1] Racket's functions contracts, [2] is also a good reference. There are two challenges/decisions:
* _strictness_, a function that ignores it's input may evaluate it anyways if the target contract does
* _strictness_, a function that ignores it input may evaluate it anyways if the target contract does
* _lax vs picky_, as pointed in [3], we can decide to wrap or not the argument on the domain contract when passed to the codomain, I think it should be checked there as well.
* Dependent records, `{idx: Bool, val: if idx then A else B}` would allow us to have Sigma types quite naturally, together with some more complex stuff.