mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-01 01:09:03 +03:00
ad632d825d
It's disappointing to have to do this, but I think necessary because various issue reports have shown it to be unsound (at least as far as inference goes) and, at the very least, confusing. This patch brings us back to the basic rules of QTT. On the one hand, this makes the 1 multiplicity less useful, because it means we can't flag arguments as being used exactly once which would be useful for optimisation purposes as well as precision in the type. On the other hand, it removes some complexity (and a hack) from unification, and has the advantage of being correct! Also, I still consider the 1 multiplicity an experiment. We can still do interesting things like protocol state tracking, which is my primary motivation at least. Ideally, if the 1 multiplicity is going to be more generall useful, we'll need some kind of way of doing multiplicity polymorphism in the future. I don't think subtyping is the way (I've pretty much always come to regret adding some form of subtyping). Fixes #73 (and maybe some others).
83 lines
2.0 KiB
Plaintext
83 lines
2.0 KiB
Plaintext
Main> Prelude.plus : Nat -> Nat -> Nat
|
|
Add two natural numbers.
|
|
@ x the number to case-split on
|
|
@ y the other numberpublic export
|
|
|
|
Totality: total
|
|
Main> Prelude.Nat : Type
|
|
Natural numbers: unbounded, unsigned integers which can be pattern matched.
|
|
|
|
Constructors:
|
|
Z : Nat
|
|
Zero.
|
|
S : Nat -> Nat
|
|
Successor.
|
|
Main> Prelude.List : Type -> Type
|
|
Generic lists.
|
|
|
|
Constructors:
|
|
Nil : List a
|
|
Empty list
|
|
:: : a -> List a -> List a
|
|
Main> Prelude.Show : Type -> Type
|
|
Things that have a canonical `String` representation.
|
|
Parameters: ty
|
|
|
|
Methods:
|
|
show : (x : ty) -> String
|
|
Convert a value to its `String` representation.
|
|
@ x the value to convert
|
|
showPrec : (d : Prec) -> (x : ty) -> String
|
|
Convert a value to its `String` representation in a certain precedence
|
|
context.
|
|
|
|
A value should produce parentheses around itself if and only if the given
|
|
precedence context is greater than or equal to the precedence of the
|
|
outermost operation represented in the produced `String`. *This is
|
|
different from Haskell*, which requires it to be strictly greater. `Open`
|
|
should thus always produce *no* outermost parens, `App` should always
|
|
produce outermost parens except on atomic values and those that provide
|
|
their own bracketing, like `Pair` and `List`.
|
|
@ d the precedence context.
|
|
@ x the value to convert
|
|
|
|
Implementations:
|
|
Show Int
|
|
Show Integer
|
|
Show Bits8
|
|
Show Bits16
|
|
Show Bits32
|
|
Show Bits64
|
|
Show Double
|
|
Show Char
|
|
Show String
|
|
Show Nat
|
|
Show Bool
|
|
Show ()
|
|
(Show a, Show b) => Show (a, b)
|
|
(Show a, Show (p y)) => Show (DPair a p)
|
|
Show a => Show (List a)
|
|
Show a => Show (Maybe a)
|
|
(Show a, Show b) => Show (Either a b)
|
|
Main> Prelude.show : Show ty => ty -> String
|
|
Convert a value to its `String` representation.
|
|
@ x the value to convert
|
|
|
|
Totality: total
|
|
Main> Prelude.Monad : (Type -> Type) -> Type
|
|
Parameters: m
|
|
Constraints: Applicative m
|
|
|
|
Methods:
|
|
>>= : m a -> (a -> m b) -> m b
|
|
Also called `bind`.
|
|
join : m (m a) -> m a
|
|
Also called `flatten` or mu.
|
|
|
|
Implementations:
|
|
Monad IO
|
|
Monad Maybe
|
|
Monad (Either e)
|
|
Monad List
|
|
Main> Bye for now!
|