Remove linearity subtyping
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).
2020-12-27 22:58:35 +03:00
|
|
|
Main> Prelude.plus : Nat -> Nat -> Nat
|
2021-04-21 11:39:18 +03:00
|
|
|
Add two natural numbers.
|
|
|
|
@ x the number to case-split on
|
|
|
|
@ y the other numberpublic export
|
|
|
|
Totality: total
|
2022-03-25 02:11:10 +03:00
|
|
|
Visibility: public export
|
2021-08-19 13:38:14 +03:00
|
|
|
Main> data Prelude.Nat : Type
|
2021-04-21 11:39:18 +03:00
|
|
|
Natural numbers: unbounded, unsigned integers which can be pattern matched.
|
|
|
|
Totality: total
|
2022-03-25 02:11:10 +03:00
|
|
|
Visibility: public export
|
2021-04-21 11:39:18 +03:00
|
|
|
Constructors:
|
|
|
|
Z : Nat
|
|
|
|
Zero.
|
|
|
|
S : Nat -> Nat
|
|
|
|
Successor.
|
2021-10-12 23:50:20 +03:00
|
|
|
Hints:
|
|
|
|
Cast Nat String
|
|
|
|
Cast Nat Integer
|
|
|
|
Cast Nat Int
|
|
|
|
Cast Nat Char
|
|
|
|
Cast Nat Double
|
|
|
|
Cast Nat Bits8
|
|
|
|
Cast Nat Bits16
|
|
|
|
Cast Nat Bits32
|
|
|
|
Cast Nat Bits64
|
|
|
|
Cast Nat Int8
|
|
|
|
Cast Nat Int16
|
|
|
|
Cast Nat Int32
|
|
|
|
Cast Nat Int64
|
|
|
|
Cast String Nat
|
|
|
|
Cast Double Nat
|
|
|
|
Cast Char Nat
|
|
|
|
Cast Int Nat
|
|
|
|
Cast Integer Nat
|
|
|
|
Cast Bits8 Nat
|
|
|
|
Cast Bits16 Nat
|
|
|
|
Cast Bits32 Nat
|
|
|
|
Cast Bits64 Nat
|
|
|
|
Cast Int8 Nat
|
|
|
|
Cast Int16 Nat
|
|
|
|
Cast Int32 Nat
|
|
|
|
Cast Int64 Nat
|
|
|
|
Eq Nat
|
|
|
|
Num Nat
|
|
|
|
Ord Nat
|
|
|
|
Range Nat
|
|
|
|
Show Nat
|
2021-08-19 13:38:14 +03:00
|
|
|
Main> data Prelude.List : Type -> Type
|
2021-04-21 11:39:18 +03:00
|
|
|
Generic lists.
|
|
|
|
Totality: total
|
2022-03-25 02:11:10 +03:00
|
|
|
Visibility: public export
|
2021-04-21 11:39:18 +03:00
|
|
|
Constructors:
|
|
|
|
Nil : List a
|
|
|
|
Empty list
|
2021-04-26 17:59:00 +03:00
|
|
|
(::) : a -> List a -> List a
|
2021-04-28 11:31:01 +03:00
|
|
|
A non-empty list, consisting of a head element and the rest of the list.
|
2021-10-12 23:50:20 +03:00
|
|
|
Hints:
|
|
|
|
Alternative List
|
|
|
|
Applicative List
|
|
|
|
Eq a => Eq (List a)
|
|
|
|
Foldable List
|
|
|
|
Functor List
|
|
|
|
Monad List
|
|
|
|
Monoid (List a)
|
|
|
|
Ord a => Ord (List a)
|
|
|
|
Semigroup (List a)
|
|
|
|
Show a => Show (List a)
|
|
|
|
Traversable List
|
2021-08-19 13:38:14 +03:00
|
|
|
Main> interface Prelude.Show : Type -> Type
|
2021-04-21 11:39:18 +03:00
|
|
|
Things that have a canonical `String` representation.
|
2021-11-02 18:34:52 +03:00
|
|
|
A minimal implementation includes either `show` or `showPrec`.
|
2021-04-21 11:39:18 +03:00
|
|
|
Parameters: ty
|
2021-08-13 18:00:54 +03:00
|
|
|
Constructor: MkShow
|
2021-04-21 11:39:18 +03:00
|
|
|
Methods:
|
2021-08-13 18:00:54 +03:00
|
|
|
show : ty -> String
|
2021-04-21 11:39:18 +03:00
|
|
|
Convert a value to its `String` representation.
|
|
|
|
@ x the value to convert
|
2021-08-13 18:00:54 +03:00
|
|
|
showPrec : Prec -> ty -> String
|
2021-04-21 11:39:18 +03:00
|
|
|
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
|
2021-06-28 22:00:10 +03:00
|
|
|
Show Int8
|
|
|
|
Show Int16
|
|
|
|
Show Int32
|
|
|
|
Show Int64
|
2021-04-21 11:39:18 +03:00
|
|
|
Show Double
|
|
|
|
Show Char
|
|
|
|
Show String
|
|
|
|
Show Nat
|
|
|
|
Show Bool
|
2021-06-23 18:15:18 +03:00
|
|
|
Show Void
|
2021-04-21 11:39:18 +03:00
|
|
|
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)
|
2022-01-19 23:19:08 +03:00
|
|
|
Show Ordering
|
2020-07-08 18:52:56 +03:00
|
|
|
Main> Prelude.show : Show ty => ty -> String
|
2021-04-21 11:39:18 +03:00
|
|
|
Convert a value to its `String` representation.
|
|
|
|
@ x the value to convert
|
|
|
|
Totality: total
|
2022-03-25 02:11:10 +03:00
|
|
|
Visibility: public export
|
2021-08-19 13:38:14 +03:00
|
|
|
Main> interface Prelude.Monad : (Type -> Type) -> Type
|
2021-11-02 18:34:52 +03:00
|
|
|
Monad
|
|
|
|
@m The underlying functor
|
|
|
|
A minimal definition includes either `(>>=)` or `join`.
|
2021-04-21 11:39:18 +03:00
|
|
|
Parameters: m
|
|
|
|
Constraints: Applicative m
|
2021-08-13 18:00:54 +03:00
|
|
|
Constructor: MkMonad
|
2021-04-21 11:39:18 +03:00
|
|
|
Methods:
|
2021-04-26 17:59:00 +03:00
|
|
|
(>>=) : m a -> (a -> m b) -> m b
|
2021-04-21 11:39:18 +03:00
|
|
|
Also called `bind`.
|
2021-08-13 18:00:54 +03:00
|
|
|
Fixity Declaration: infixl operator, level 1
|
2021-04-21 11:39:18 +03:00
|
|
|
join : m (m a) -> m a
|
|
|
|
Also called `flatten` or mu.
|
|
|
|
Implementations:
|
|
|
|
Monad IO
|
|
|
|
Monoid a => Monad (Pair a)
|
|
|
|
Monad Maybe
|
|
|
|
Monad (Either e)
|
|
|
|
Monad List
|
2021-03-12 12:46:46 +03:00
|
|
|
Main> 1 : Integer
|
2021-11-18 21:13:20 +03:00
|
|
|
Primitive unsigned int value (backend-dependent precision)
|
2021-10-13 13:45:39 +03:00
|
|
|
Main> String : Type
|
2021-10-13 14:10:32 +03:00
|
|
|
Primitive type of strings
|
2021-10-13 13:45:39 +03:00
|
|
|
Hints:
|
|
|
|
Cast Int String
|
|
|
|
Cast Integer String
|
|
|
|
Cast Char String
|
|
|
|
Cast Double String
|
|
|
|
Cast Nat String
|
|
|
|
Cast Int8 String
|
|
|
|
Cast Int16 String
|
|
|
|
Cast Int32 String
|
|
|
|
Cast Int64 String
|
|
|
|
Cast Bits8 String
|
|
|
|
Cast Bits16 String
|
|
|
|
Cast Bits32 String
|
|
|
|
Cast Bits64 String
|
|
|
|
Cast String Integer
|
|
|
|
Cast String Int
|
|
|
|
Cast String Double
|
|
|
|
Cast String Bits8
|
|
|
|
Cast String Bits16
|
|
|
|
Cast String Bits32
|
|
|
|
Cast String Bits64
|
|
|
|
Cast String Int8
|
|
|
|
Cast String Int16
|
|
|
|
Cast String Int32
|
|
|
|
Cast String Int64
|
|
|
|
Cast String Nat
|
|
|
|
Eq String
|
|
|
|
FromString String
|
2021-10-13 19:26:54 +03:00
|
|
|
Interpolation String
|
2021-10-13 13:45:39 +03:00
|
|
|
Monoid String
|
|
|
|
Ord String
|
|
|
|
Semigroup String
|
|
|
|
Show String
|
|
|
|
Main> Integer : Type
|
2021-10-13 14:10:32 +03:00
|
|
|
Primitive type of unbounded signed integers
|
2021-10-13 13:45:39 +03:00
|
|
|
Hints:
|
|
|
|
Abs Integer
|
|
|
|
Cast Integer String
|
|
|
|
Cast Int Integer
|
|
|
|
Cast Char Integer
|
|
|
|
Cast Double Integer
|
|
|
|
Cast String Integer
|
|
|
|
Cast Nat Integer
|
|
|
|
Cast Bits8 Integer
|
|
|
|
Cast Bits16 Integer
|
|
|
|
Cast Bits32 Integer
|
|
|
|
Cast Bits64 Integer
|
|
|
|
Cast Int8 Integer
|
|
|
|
Cast Int16 Integer
|
|
|
|
Cast Int32 Integer
|
|
|
|
Cast Int64 Integer
|
|
|
|
Cast Integer Int
|
|
|
|
Cast Integer Char
|
|
|
|
Cast Integer Double
|
|
|
|
Cast Integer Bits8
|
|
|
|
Cast Integer Bits16
|
|
|
|
Cast Integer Bits32
|
|
|
|
Cast Integer Bits64
|
|
|
|
Cast Integer Int8
|
|
|
|
Cast Integer Int16
|
|
|
|
Cast Integer Int32
|
|
|
|
Cast Integer Int64
|
|
|
|
Cast Integer Nat
|
|
|
|
Eq Integer
|
|
|
|
Integral Integer
|
|
|
|
Neg Integer
|
|
|
|
Num Integer
|
|
|
|
Ord Integer
|
|
|
|
Show Integer
|
|
|
|
Main> Bits16 : Type
|
2021-10-13 14:10:32 +03:00
|
|
|
Primitive type of 16 bits unsigned integers
|
2021-10-13 13:45:39 +03:00
|
|
|
Hints:
|
|
|
|
Abs Bits16
|
|
|
|
Cast Bits16 String
|
|
|
|
Cast Bits16 Integer
|
|
|
|
Cast Bits16 Int
|
|
|
|
Cast Bits16 Char
|
|
|
|
Cast Bits16 Double
|
|
|
|
Cast Bits16 Bits8
|
|
|
|
Cast Int Bits16
|
|
|
|
Cast Integer Bits16
|
|
|
|
Cast Bits8 Bits16
|
|
|
|
Cast Bits32 Bits16
|
|
|
|
Cast Bits64 Bits16
|
|
|
|
Cast String Bits16
|
|
|
|
Cast Double Bits16
|
|
|
|
Cast Char Bits16
|
|
|
|
Cast Nat Bits16
|
|
|
|
Cast Int8 Bits16
|
|
|
|
Cast Int16 Bits16
|
|
|
|
Cast Int32 Bits16
|
|
|
|
Cast Int64 Bits16
|
|
|
|
Cast Bits16 Bits32
|
|
|
|
Cast Bits16 Bits64
|
|
|
|
Cast Bits16 Int8
|
|
|
|
Cast Bits16 Int16
|
|
|
|
Cast Bits16 Int32
|
|
|
|
Cast Bits16 Int64
|
|
|
|
Cast Bits16 Nat
|
|
|
|
Eq Bits16
|
|
|
|
Integral Bits16
|
|
|
|
Neg Bits16
|
|
|
|
Num Bits16
|
|
|
|
Ord Bits16
|
|
|
|
Show Bits16
|
2020-07-08 17:52:57 +03:00
|
|
|
Main> Bye for now!
|