From 950466c3e87dbe0d5c4df1af4a1818f9dd0f364b Mon Sep 17 00:00:00 2001 From: James Martin Date: Mon, 29 Mar 2021 22:12:58 -0700 Subject: [PATCH] More WIP on the new syntax, but I think I might go in a different direction now. --- examples/examples.ivo | 175 +++++++- src/Ivo/Syntax/Base.hs | 910 +++++---------------------------------- src/Ivo/Syntax/Parser.hs | 2 + 3 files changed, 268 insertions(+), 819 deletions(-) diff --git a/examples/examples.ivo b/examples/examples.ivo index c809d61..4ed8ae1 100755 --- a/examples/examples.ivo +++ b/examples/examples.ivo @@ -1,26 +1,173 @@ #!/usr/bin/env -S ivo -c + +// syntax for algebraic data types +type ℕ + + 0 + + 1+ ℕ + +type List a + + [] + + _∷_ a (List a) + +// syntax for algebraic codata types +type Stream a + & Head a + & Tail (Stream a) + +// syntax for generalized algebraic (co)data types +type Vec a : ℕ → Type + [] : Vec a 0 + _∷_ : ∀ n → a → Vec a n → Vec a (1+ n) + +// syntax for mutually-recursive types +types + Even Odd : ℕ → Type + + 0even : Even 0 + 1+odd : ∀ n → Odd n → Even (1+ n) + 1+even : ∀ n → Even n → Odd (1+ n) + +// syntax for higher-inductive type +type Multiset a + empty : Multiset a + singleton : a → Multiset a + append : Multiset a → Multiset a → Multiset a + + append_commutative : (x y : Multiset a) → append x y ≡ append y x + +// syntax for inductive-recursive types? (needs work) +types a _#_ + DList : Type + Fresh : a → Dlist a → Type + + [] : DList a + _∷_#_ : (head : a) → (tail : DList a) → Fresh head tail → DList a + + fresh[] : (x : a) → Fresh x [] + fresh∷ : (x : a) → (head : a) → (tail : DList a) → (p : Fresh head tail) → x # head → Fresh x tail → Fresh x (head ∷ tail # p) + +// syntax for traits +trait Functor f + map : ∀ a b → (a → b) → f a → f b + +// short for `open data type List a` +// short for `open implicit trait Functor f` + +// generated signatures +sig + ℕ : Type + ℕ_Sig : Sig + ℕ_Impl : ℕ_Sig + + 0 : ℕ + 1+ : ℕ → ℕ + + pattern 0 1+ + complete 0 1+ + + ℕ_rec : ∀ a ⇒ a → ( a → a ) → ℕ → a + ℕ_ind : (C : ℕ → Type) ⇒ C 0 → (∀ n → C n → C (1+ n)) → (n : ℕ) → C n + +recurse : Sig → ... +induct : Sig → ... +baseFunctor : Sig → Sig + +sig + Functor : Type → Sig + + map : ∀ f ⇒ Functor f ⇒ ∀ a b ⇒ (a → b) → f a → f b + + +inductive type + +type List a + + [] + + _:+_ a (List a) + +type Stream a + & Head a + & Tail (Stream a) + +type Vec a : ℕ → Type + [] : Vec a 0 + _:+_ : ∀ n → a → Vec a n → Vec a (1+ n) + +sig + ℕ : Type + Z : ℕ + S : ℕ → ℕ + +sig + List : Type → Type + [] : ∀ a → List a + _:+_ : ∀ a → a → List a → List a + +sig + Stream : Type → Type + Head : ∀ a → Stream a → a + Tail : ∀ a → Stream a → Stream a + +iterate : ∀ a → (a → a) → a → ℕ → a +iterate f x + 0 → [] + 1+ n → x :+ iterate f (f x) n + +iterate = \ f x n → case n { + 0 → []; + 1+ n → x :+ iterate f (f x) n; +}; + +iterate f x = \case + 0 -> [] + 1+ n -> x : iterate f (f x) n + +append : ∀ a → List a → List a → List a +append xs ys = case xs + [] → ys + x :+ xs → x :+ append xs ys + +reverse : ∀ a → List a → List a +reverse + [] → [] + x :+ xs → append (reverse xs) [ x ] + +churchℕ : Type +churchℕ = ∀ a → (a → a) → a → a + +churchS : churchℕ → churchℕ +churchS n f x = f (n f x) + +church+ : churchℕ → churchℕ → churchℕ +church+ n = n churchS + // Create a list by iterating `f` `n` times: -letrec iterate = \f x. - { Z -> [] - ; S n -> (x :: iterate f (f x) n) - }; +iterate = λ f x { + Z → []; + 1+ n → x :+ iterate f (f x) n; +}; // Use the iterate function to count to 10: -let countToTen : [Nat] = - let countTo = iterate S 1 +countToTen : [Nat] = + let countTo = iterate +1 1 in countTo 10; // Append two lists together: -letrec append = \xs ys. - { [] -> ys - ; (x :: xs) -> (x :: append xs ys) - } xs; +append = λ xs ys → case xs { + [] → ys; + x :+ xs → x :+ append xs ys; +}; // Reverse a list: -letrec reverse = - { [] -> [] - ; (x :: xs) -> append (reverse xs) [x] - }; +reverse = λ { + [] → []; + _:+_ x xs → append (reverse xs) [ x ] +}; + +// Basic operations on church-encoded naturals. +churchS = λ n f x → f (n f x); +church+ = λ n → n churchS; + +main = // Now we can reverse `"reverse"`: let reverseReverse : [Char] = reverse "reverse"; diff --git a/src/Ivo/Syntax/Base.hs b/src/Ivo/Syntax/Base.hs index ccb3e97..410fd84 100644 --- a/src/Ivo/Syntax/Base.hs +++ b/src/Ivo/Syntax/Base.hs @@ -1,5 +1,9 @@ -- | The language's abstract syntax. -- +-- This source code does not document the concrete syntax in any detail; +-- please refer to the language reference for more information about that. +-- +-- This abstract syntax may include features which have not been implemented yet. -- The abstract syntax is very forward-thinking -- in that it's designed to accomodate for features -- which haven't been implemented yet, @@ -22,453 +26,149 @@ module Ivo.Syntax.Base import Data.List.NonEmpty (NonEmpty (..)) import Data.Text (Text) -newtype Scope = Scope [TopLevel] +newtype Scope = Scope [Definition] deriving Show -data TopLevel - -- | Bring the definitions in a module into scope. - -- - -- > open Module1 - -- - -- An explicit import list is also permitted: - -- - -- > open Module2 ( foo ; bar ; baz ) - -- - -- All of the imports can be re-exported using @pub open@, - -- or individual imports may be made public - -- by individually prefixing each with @pub@. - -- These syntaxes may not be combined. - -- - -- > pub open Module1 ; - -- > open Module2 ( pub foo ; bar ; pub baz ) ; - -- - -- Fields can additionally be renamed or hidden: - -- - -- > open Module3 using ( foo ; bar ) renaming ( foo → baz ) ; - -- > open Module4 hiding ( foo ) ; - -- > open Module5 hiding ( foo ) renaming ( bar → baz ) ; - -- - -- Combining an explicit import list with a hiding list is forbidden, - -- seeing as doing so would be completely pointless. - -- - -- It is also possible to open signatures, but only into other signatures. - -- When opening into a signature, all declarations are added to - -- the enclosing signature's declarations /regardless/ of - -- whether the open was marked public, - -- but default definitions are imported only as part of a @pub open@. - -- - -- Note that this feature may be used as part of this idiom for extending a module: - -- - -- > Λ m → sig Monoid { - -- > pub open Semigroup m ; - -- > ∅ : m ; - -- > // ... identity laws --- - -- > } - -- - -- Data constructor patterns are exported - -- separately from the constructors themselves. - -- The patterns are exported under the type constructor's name; - -- the constructors are exported like functions. - -- Exporting patterns implicitly exports the constructors as well, - -- but the constructors can subsequently be hidden. - -- Here's what I mean: - -- - -- > // export both constructors and patterns: - -- > open data using ( MyType ( Con1 ; Con2 ) ) ; - -- > // export just constructors, not patterns: - -- > open data using ( MyType ; Con1 ; Con2 ) ; - -- > // export just patterns, not constructors: - -- > open data using ( MyType ( Con1 ; Con2 ) ) hiding ( Con1 ; Con2 ) ; - -- > // export the patterns and data constructors, but not the type constructor: - -- > open data using ( MyType ( Con1 ; Con2 ) ) hiding ( MyType ) ; - -- - -- Combined with default definitions in the signature - -- (to whom both the constructors and patterns are /always/ in scope) - -- this can be used to implement opaque data types - -- with smart constructors and/or eliminators, - -- because the type could only be constructed via exported default functions, - -- but pattern matched against as usual (or vice versa, or both). - -- - -- An "import all" syntax is also supported: - -- - -- // import all constructors - -- > open data using ( MyType ( .. ) ) ; - -- // hide all constructors - -- > open data hiding ( MyType ( .. ) ) ; - -- - -- This uses 'FlexibleSeparatorSyntax'. - = Open PublicOrPrivate Expr [(Text, Maybe (Maybe [Text]))] -- * @using@ - [(Text, Maybe (Maybe [Text]))] -- * @hiding@ - [(Text, Text)] -- * @renaming@ - -- | See 'Definition'. - -- - -- A definition may be exported from the enclosing module or signature - -- by prefixing it with the keyword @pub@: - -- - -- > pub foo : bar = baz - | Define PublicOrPrivate Definition - -- | At the top level, @data @ is syntactic sugar for @open data @. - -- - -- See 'Open' and 'Data' for more information.. - | TLData Expr - -- | At the top level, @axiom @ is syntactic sugar for @open axiom @. - -- - -- See 'Open' and 'Axiom' for more information. - | TLAxiom Expr - -- | At the top level, @adt <...>@, @gadt <...>@, and @sig <...>@ - -- are syntactic sugar for @open data adt <...>@, @open data gadt <...>@, - -- and @open data sig <...>@ respectively. - -- - -- See 'Open', 'Data', and 'Sig' for more information. - | TLSig Sig - deriving Show +data Definition = Definition Visibility Item -- | 'Public' is written with @pub@; -- 'Private' indicates the abscence of an access modifier. -data PublicOrPrivate = Public | Private +data Visibility = Public | Private + +data Item + -- | @ = @ + -- or @ @ + = Def Text [Pattern] CaseBranches + -- | @ : @ + | Decl (NonEmpty Text) Type + -- | @open ? ? ? + | Open Expr (Maybe OpenUsing) (Maybe OpenHiding) (Maybe OpenRenaming) + -- | @ = @ + | PatSyn Bool Text [Text] Pattern + -- | @ [: ]?@ + | PatDecl Bool [Text] (Maybe Type) + -- | @complete [: ]?@ + | Complete [Text] (Maybe Type) + -- | @infix @ + | FixityDecl Fixity (NonEmpty Text) + -- | @implicit [: ]?@ + | Implicit Expr (Maybe Type) + -- | @data @ + | DataStmt Expr + -- | @axiom @ + | AxiomStmt Expr + -- | @axioms @ + | AxiomsStmt Scope + -- | @type @ + | TypeStmt TypeDecl + -- | @types @ + | TypesStmt Scope + -- | @trait @ + | TraitStmt TraitDecl + -- | @record @ + | RecordStmt RecordImpl deriving Show --- | Define a name as an expression, with an optional type annotation. --- --- > foo : type = ; // with type annotation --- > bar = ; // with inferred type -data Definition = Definition Text (Maybe Type) Expr - deriving Show +-- | @using (pub? pat? ; ...)@ +type OpenUsing = [(Visibility, Bool, Text)] + +-- | @hiding (complete + or @pat? ; ...)@ +type OpenHiding = [Either [Text] (Bool, Text)] + +-- | @renaming (pat? → pub? ? ; ...)@ +type OpenRenaming = [(Text, Text)] + +-- | @fixity ? @ +data Fixity = Fixity (Maybe Associativity) Precedence + +-- | @@ +data Associativity = AssocLeft | AssocRight + +-- | @<+|->?digit+[.digit+]?@ +type Precedence = Text -- | An expression which represents the type of a type. type Kind = Type - deriving Show -- | An expression which represents the type of a value. type Type = Expr + | Complete [Text] (Maybe Type) + -- | @infix @ + | FixityDecl Fixity (NonEmpty Text) + -- | @implicit [: ]?@ + | Implicit Expr (Maybe Type) + -- | @data @ + | DataStmt Expr + -- | @axiom @ + | AxiomStmt Expr + -- | @axioms @ + | AxiomsStmt Scope + -- | @type @ + | TypeStmt TypeDecl + -- | @types @ + | TypesStmt Scope + -- | @trait @ + | TraitStmt TraitDecl + -- | @record @ + | RecordStmt RecordImpl deriving Show -data Expr - --- - --- Expressions pertaining to signatures and modules - --- +-- | @using (pub? pat? ; ...)@ +type OpenUsing = [(Visibility, Bool, Text)] - -- | Automatically implement a signature by creating (co)inductive data types - -- with the given constructors/eliminators, and additionally pattern matching. - -- - -- > data - -- - -- See 'ADT', 'GADT', and 'Sig' for examples of the data types this can implement. - -- - -- @data@ can be used to implement things with kind @Type → ... → Sig@ - -- by turning all type arguments into signature parameters, - -- but generally speaking, the use of signature parameters should be preferred - -- see 'Sig' (the type, not the constructor). +-- | @hiding (complete + or @pat? ; ...)@ +type OpenHiding = [Either [Text] (Bool, Text)] + +-- | @renaming (pat? → pub? ? ; ...)@ +type OpenRenaming = [(Text, Text)] + +-- | @fixity ? @ +data Fixity = Fixity (Maybe Associativity) Precedence + +-- | @@ +data Associativity = AssocLeft | AssocRight + +-- | @<+|->?digit+[.digit+]?@ +type Precedence = Text + +-- | An expression which represents the type of a type. +type Kind = Type +-- | An expression which represents the type of a value. +type Type = Expr + +data Expr = Data Expr - -- | Automatically "implement" a signature by taking all of its definitions as axioms. - -- - -- > axiom - -- - -- Axiom "implementations" do not have any computational meaning - -- and can only be typechecked, but not executed. - -- It may be possible to execute a program which contains axioms, - -- but the program will crash when the axioms are encountered. - -- - -- Axioms are useful when writing proofs which you are not interested in executing, - -- or as placeholders for functions you haven't implemented yet. | Axiom Expr -- | A signature literal. See 'ADT', 'GADT', and 'Sig' for examples. | SigE Sig - -- | A module expression with an optional signature annotation. - -- Like with signatures, modules may have type parameters. - -- - -- If a module has a signature annotation, - -- then only the names in the signature will be exported - -- (and /all/ of those names will, even if they were not marked public - -- at their definition site). - -- All names exposed by the signature will be typechecked - -- against their types in the signature. - -- - -- If no signature is specified, then the module will have an anonymous signature - -- based on the inferred (or specified) types for all of its public definitions. - -- - -- > Λ a → mod : Monoid (List a) { - -- > ∅ = [] ; - -- > _<>_ = /* don't feel like writing this code right now */ ; - -- > - -- > monoid_id_left = ... ; - -- > ... - -- > } - -- - -- Like with most scopes, it is possible to open a module within another module; - -- public imports will be re-exported if specified by the module's signature. - -- - -- A public definition which is not included in the module's signature - -- will issue a warning, but not fail to compile. - -- Because definitions are exported if and only if they are part of the signature, - -- @pub@ is always redundant in a module with a type signature. - -- - -- This uses 'FlexibleSeparatorSyntax'. | Mod [Either (NonEmpty Text, Kind) Text] (Maybe Type) [TopLevel] - -- | A field accessor for signatures and modules. - -- - -- A signature @sig : Sig@ which defines @foo : bar@ - -- and a module implementing that signature @mod : sig@, then: - -- - -- > sig::foo : sig → bar - -- > mod::foo : bar | Access Expr Text --- --- Expressions pertaining to types --- - -- | Universal type quantification with optional kind annotations. - -- - -- With unicode syntax: - -- - -- > ∀ foo ( bar : baz ) quux → type - -- - -- With ASCII syntax: - -- - -- > forall foo ( bar : baz ) quux -> type - -- - -- Forall is constructed by 'TypeLam' and eliminated by 'TypeApp'; - -- however, occurrences of 'TypeLam' and 'TypeApp' - -- will usually be inferred and do not need to be written. - -- - -- 'Forall' is used for abstracting over /computationally-irrelevant/ terms; - -- the terms are usually dependent and invisible, but /may/ not be. - -- - -- 'Arrow' is used for abstracting over /computationally-relevant/ terms; - -- the terms are always visible and usually independent, but /may/ be. - -- - -- The distinction between these quantifiers was first made known to me - -- by Sam Lindley and Conor McBride's Hasochism paper. | Forall (NonEmpty (Either (NonEmpty Text, Kind) Text)) Type - -- | Function types with optional argument names; - -- multiple arguments may be bound with one type. - -- - -- With unicode syntax: - -- - -- > ( foo bar : baz ) → quux → fwee - -- - -- With ASCII syntax: - -- - -- > ( foo bar : baz ) -> quux -> fwee - -- - -- Arguments @foo@ and @bar@ both have type @baz@; - -- the argument with type @quux@ does not have a name; - -- @fwee@ is the function's return type. - -- - -- Note that an empty list of argument names - -- corresponds with @foo → bar@, /not/ @(: foo) → bar@, - -- which is syntactically invalid. - -- - -- 'Arrow' is constructed by 'Lam' and eliminated by 'App'. - -- - -- 'Arrow', as a relevant quantifier, contrasts 'Forall', an irrelevant quantifier; - -- more information in the documentation for 'Forall'. | Arrow [Text] Type Type -- | Type annotations (or kind annotations; they are the same thing). -- -- > foo : bar | Ann Expr Type - -- | A hole represents a type or value to be inferred. - -- If inference fails, then the inferred type or kind - -- and detailed information about the surrounding context will be printed as an error, - -- to be used as a tool for type-driven development. - -- - -- > _ | Hole --- --- Expressions pertaining to values --- - -- | The constructor for 'Forall', - -- which explicitly binds a forall-quantified type variable - -- as a value-level variable with an optional kind annotation. - -- - -- With unicode syntax: - -- - -- > Λ a → foo : ∀ a → bar - -- > Λ ( a : k ) → foo : ∀ ( a : k ) → bar - -- - -- With ASCII syntax: - -- - -- > ^ a -> foo : forall a -> bar - -- > ^ ( a : k ) -> foo : forall ( a : k ) -> bar - -- - -- The name of the variable and the type and in the value - -- do not have to be the same, and in these specific examples, - -- there is no need whatsoever to annotate the kind in both - -- the type and value; if one is specified, the other will - -- /always/ be able to be inferred. - -- - -- These variables still are type variables and do not contain data; - -- they will be completely erased at runtime so the computational behavior - -- of a function cannot depend on them. - -- - -- Type lambdas are usually inferred and do not need to be written down. - -- The purpose of type lambdas is to bring type variables into scope - -- for use by type annotations and type applications. - -- - -- In the presence of inferred type lambdas, - -- the explicit type lambda will always bind the /innermost/ forall. - -- There are a few reasons for this: - -- - -- 1. Type quantifiers can only depend on types to their left, - -- meaning that the innermost quantifiers tend to be the most complex - -- and most difficult to infer. - -- - -- 2. If the kind of a quantified type is inferred to be polymorphic, - -- a new kind variable will be introduced and quantified - -- on the /left/ for the reasons described in (1). - -- These implicitly-quantified variables /cannot/ - -- be bound by type lambdas or applied using type applications, - -- but even if they could be, binding quantifiers inner-to-outer - -- would prevent this transformation from affecting - -- the meaning of the expression. - -- - -- 3. Module parameters may be given specific values - -- /or/ be made polymorphic, depending on how the module is used. - -- These inserted foralls are inserted (obviously) on the /left/. | TypeLam (NonEmpty (Either (NonEmpty Text, Kind) Text)) Expr - -- | Type application, the eliminator for 'Forall'. - -- - -- Suppose you have an expression @foo : forall a → bar a@, - -- but the type @a@ is ambiguous and cannot be inferred. - -- You may explicitly instantiate @foo@ with @Nat@: - -- - -- > foo @ Nat : bar Nat - -- - -- Type application can usually be inferred without needing to be specified. | TypeApp Expr Type - -- | An lambda abstraction, the constructor for 'Arrow'. - -- - -- With unicode syntax, if @baz : quux@: - -- - -- > λ foo → baz : bar → quux - -- > λ ( foo : bar ) → baz : bar → quux - -- - -- With ASCII syntax: - -- - -- > λ foo -> baz - -- > λ ( foo : bar ) -> baz - -- - -- A lambda expression may pattern match against its arguments: - -- - -- > λ _ → foo // the argument is irrelevant - -- > λ x y → foo // multiple arguments - -- > λ ( x , y ) → foo // pattern match against a *-pair (data) - -- > λ ( π₂ → y ) → foo // project the first argument of an &-pair (codata) - -- - -- As a special case, a lambda which matches an impossible pattern - -- may have no body: - -- - -- > λ ! // that's really the whole thing! - -- - -- Even more generally, it may branch based on the pattern match, - -- after binding any number of arguments which it doesn't branch on, - -- which will be shared across every case branch. - -- - -- > λ (x , y) { - -- > S n | Left m → f n m ; - -- > Z | Right z → x z ; - -- > _ | _ → y ; - -- > } - -- - -- Pattern matching is a very complex syntactic construct - -- which can do even more than just this; - -- see 'CaseBranch' for the full detail of what it can do. - -- - -- Although the 'Lam' constructor allows for either - -- the list of patterns (for non-branching arguments) - -- or the list of case branches (for branching arguments) - -- to be empty, /at least one/ must consume an argument; - -- both may not be empty. | Lam [Pattern] [CaseBranch] -- | A lambda with only one, trivial branch, e.g. @λ x y z -> e@. -- -- See 'Lam'. | LamBlock [Pattern] Expr - -- | Function application, the eliminator for 'Arrow'. - -- (See also 'AppI', mixfix function application.) - -- - -- Syntactically, function application is represented by juxtiposition. - -- - -- If @foo : baz -> quux@ and @bar : baz@: - -- - -- > foo bar : quux | App Expr (NonEmpty Expr) - -- | Mixfix function application (see also 'App'). - -- - -- A mixfix operator name is composed of text - -- plus underscores where the arguments go. - -- Here, we replace the underscores with a space - -- corresponding with each argument in the list, - -- and, in the case of a partially applied mixfix operator, - -- leave the underscores for each argument /not/ applied. - -- - -- Here's a fully applied example for @if_then_else_@: - -- - -- > if foo then bar else baz - -- - -- This is a single infix application: @AppI "if then else " [foo, bar, baz]@. - -- - -- On the other hand, if we only provide the @then@ case: - -- - -- > if_then bar else_ - -- - -- This is represented as @AppI "if_then else_" [bar]@. - -- - -- If a mixfix operator is left completely unapplied, @if_then_else_@, - -- then it should be parsed as a regular variable name - -- and applied using regular function application. | AppI Text (NonEmpty Expr) - -- | A let expression, used to define variables in a local scope. - -- - -- The definitions in a let expression can include both variable definitions - -- and /opening modules/ (and consequently, even local data types). - -- - -- Defining two variables: - -- - -- > let foo = bar ; baz : quuz = splee in fwap - -- - -- Opening a module and defining a variable: - -- - -- > let open Module ; foo = bar in baz - -- - -- The definitions in a let expression may be recursive, interdependent, - -- or even mutually recursive, just like top-level declarations. - -- (However, the use of these features may interfere with type inference.) - -- Variables bound in a let expression may shadow variables, - -- including those defined by /other/ let expressions, - -- but a variable can only be defined at most once in a single let expression. - -- - -- This uses 'FlexibleSeparatorSyntax'. | Let [TopLevel] Expr - -- | A case expression, used to pattern match against some variables. - -- - -- Multiple expressions to be matched against are separated by bars (@|@) - -- with 'FlexibleSeparatorSyntax'. - -- - -- > case foo | bar { - -- > π₁ ( Left x | _ ) → x ; - -- > π₁ ( Right _ | z ) → z ; - -- > π₂ ( Right y | _ ) → y ; - -- > π₂ ( Left _ | z ) → z ; - -- > } - -- - -- A case expression with no arguments may be used just for guards: - -- - -- > case { - -- > ? cond1 → x ; - -- > ? cond2 → y ; - -- > ? else → z ; - -- > } - -- - -- 'Lam' may also perform case branching; lambda case syntax - -- should generally be preferred over binding a variable with lambda - -- and then immediately 'Case'-ing it. - -- - -- For more information about the (very complex) syntax of case branches, - -- see 'CaseBranch'. | Case [Expr] [CaseBranch] -- | A case with only one, trivial branch, e.g. -- @case x | y of a , b | c , d → e@. @@ -481,406 +181,38 @@ data Expr | Var Text deriving Show --- | A signature literal. --- --- Signatures are the type of modules. --- They're basically record types, --- associating a bunch of names with a bunch of types. --- --- Signatures can be used for many things, including defining data types. --- See 'Data', 'Axiom', and 'Mod' for a few ways they can be used. --- --- However, there are multiple syntaxes for writing them, --- which is (obviously) what this type enumerates. --- --- Do not confuse type functions which return a signature (@Λ a → @), --- signature parameters (@sig a { ... }@), --- and type indices (@sig { Foo : a → Type }@)! --- These three features serve entirely different purposes. --- --- Type functions which return a signature /are not signatures per se/ --- and /must/ be instantiated with a type argument to become a signature. --- The created signature is /not/ polymorphic over the bound type. --- --- For example, this signature describes for any type @m@ that @m@ is a semigroup: --- --- > Λ m → sig { --- > _<>_ : m → m → m ; --- > <>IsAssoc : ( x y z : m ) → ( x <> y ) <> z ≡ x <> ( y <> z ) ; --- > --- --- Signature parameters are universally quantified --- across all definitions in the signature, --- so that the signature may reference its own definitions with any type parameter, --- and critically, the /implementation/ must be polymorphic over the --- signature parameter as well. --- --- The way quantifiers work is that they're added as /explicit/ parameters to kinds --- and as /implicit/ parameters to types for all declarations and definitions --- in the signature. --- --- For example, this signature describes a list data type --- which works for any type @a@, plus a @join@ operation: --- --- > sig a { --- > List : Type ; --- > [] : List a ; --- > _∷_ : List a → List a → List a ; --- > join : List (List a) → List a ; --- > } --- --- Note that the @join@ operation would be illegal for @Λ a → sig { ... }@ --- because the signature's implementation doesn't have to be polymorphic in @a@, --- but @join@ instantiates @a@ with @List a@. --- --- It is the difference between describing a polymorphic type --- and a family of monomorphic types which isn't necessarily universally implemented. --- --- Finally, type indices are just the arguments to a type constructor --- which are not quantified by @sig@ (but rather by each individual definition) --- and thus are not necessarily parametric, e.g.: --- --- > sig { --- > Fin : Nat → Type ; --- > --- > FZ : Fin Z ; --- > FS : ∀ n → Fin n → Fin ( S n ) ; --- > } data Sig - -- | Every kind of signature literal allows - -- for type parameters with optional kind signatures, - -- so those have been factored out into this constructor. = SigQs [Either (NonEmpty Text, Kind) Text] Sig' deriving Show --- | A signature literal variant, excluding type parameters. --- --- ('SigQs' is the constructor with the type parameters.) + data Sig' - -- | An algebraic data type (ADT) signature. @False@ for data, @True@ for codata. - -- - -- > adt Nat { Z + S Nat } - -- > adt Stream a { Head a & Tail ( Stream a ) } - -- - -- Preceding @+@s and @&@s are also permitted, which looks like this: - -- - -- The syntax @+@ and @&@ were chosen because the branches of ADTs correspond with - -- additive disjunction (written @⊕@ or @+@) and additive conjunction (written @&@) - -- from linear logic. - -- - -- (The arguments correspond with multiplicative conjunction (@⊗@ or @*@), - -- and multiplicative disjunction (@⅋@ or @|@) respectively; - -- however, these arguments are written using mere juxtaposition - -- instead of using an explicit syntax because it is unambiguous.) - -- - -- This uses 'FlexibleSeparatorSyntax', e.g.: - -- - -- > adt List a { - -- > + [] - -- > + _∷_ a ( List a ) - -- > } = ADT Bool Text (Maybe Kind) [(Text, [Type])] - -- | A generalized algebraic data type (GADT) signature. - -- - -- GADTs are similar to ADTs. However, thanks to their extended syntax, - -- they also may be non-parametric in their type arguments - -- (non-parametric arguments, i.e. indices, are specified in the kind signature), - -- or be used to define higher-inductive types. - -- - -- `Vec a n` has a type parameter `a` and a type index `n`: - -- - -- > gadt Vec a : Nat → Type { - -- > [] : Vec a Z ; - -- > _∷_ : ∀n. a → Vec a n → Vec a ( S n ) ; - -- - -- `Multiset a` is a higher-inductive type with a commutative `union` constructor. - -- - -- > gadt Multiset a { - -- > empty : Set a ; - -- > singleton : a → Set a ; - -- > _union_ : Set a → Set a → Set a ; - -- > - -- > // An additional constructor for Multiset's *identity* type. - -- > union_commutative : ( xs ys : Set a ) → xs union ys ≡ ys union xs; - -- > } - -- - -- This uses 'FlexibleSeparatorSyntax'. | GADT Text (Maybe Kind) [(NonEmpty Text, Type)] - -- | The most general syntax for signatures. - -- - -- General signatures are simply collections of names and their types. - -- They are not necessarily the template for a /data/ type; - -- they may also be used for defining typeclasses, - -- an abstract interface for multiple implementations of a data structure, - -- a set of definitions to be taken as axiomatic, etc. - -- - -- However, general signatures still /can/ be used to define data types - -- which are potentially more general than even GADTs, - -- for example mutually recursive types or inductive-inductive types. - -- - -- A signature which describes the Monoid typeclass: - -- - -- > sig m { - -- > empty : m ; - -- > _<>_ : m -> m -> m ; - -- > - -- > monoid_id_left : ( y : m ) → empty <> y ≡ y ; - -- > monoid_id_right : ( x : m ) → x <> empty ≡ x ; - -- > monoid_assoc : ( x y z : m ) → x <> (y <> z) ≡ (x <> y) <> z ; - -- > } - -- - -- A signature which describes an axiom, the law of the excluded middle: - -- - -- > sig a { lem : ¬ a + a } - -- - -- The simultaneous definition of two mutually-recursive data types: - -- - -- > sig { - -- > Even , Odd : Nat → Type ; - -- > - -- > zeroIsEven : Even Z ; - -- > succOddIsEven : ∀n. Odd n → Even ( S n ) ; - -- > succEvenIsOdd : ∀n. Even n → Odd ( S n ) ; - -- > } - -- - -- (Multiple comma-separated declarations use 'FlexibleSeparatorSyntax'.) - -- - -- An inductive-recursive pair of types: - -- - -- > // An inductive-recursive pair of types: - -- > open data sig ( a : Type ) ( _#_ : a → a → Type ) { - -- > // A list in which all elements are distinct from each other - -- > // by the distinctness relation `_#_`. - -- > Dlist : Type ; - -- > // A proof that the first argument is distinct - -- > // from all of the elements of the second argument. - -- > Fresh : a → Dlist a _#_ → Type ; - -- > - -- > nil : Dlist a _#_ ; - -- > cons : ( x : a ) → ( xs : Dlist a _#_ ) → Fresh a _#_ x xs → Dlist a _#_ ; - -- > - -- > freshNil : ( x : a ) → Fresh a _#_ x nil ; - -- > freshCons : ( x : a ) - -- > // the original list - -- > → ( head : a ) → ( tail : Dlist a _#_ ) → ( p : Fresh a _#_ head tail ) - -- > // `x` is distinct from both the head and tail of the original list - -- > → x # head -> Fresh a _#_ x tail - -- > // thus `x` is distinct from the /entire/ original list. - -- > → Fresh a _#_ x ( cons head tail p ) ; - -- > } - -- - -- Adding yet more complexity, signatures may also contain a default implementation, - -- which is a definition, rather than a type declaration. - -- Even further, the type of the default implementation may be a supertype of - -- the declared type of the field, so that the default implementation - -- may only be used if the definitions of other fields - -- allow the default implementation's type to unify with the declared type. - -- - -- If the default implementation's type is identical to the declared type, - -- then it is sufficient to only include the default implementation's definition; - -- that the field is part of the signature is implied by its definition. - -- - -- For typechecking purposes, the equality of signatures - -- is based only on the declared types of fields - -- (including fields implicitly declared by a definition) - -- and the definitions themselves are completely ignored; - -- for the purposes of implementing a module, - -- the default definitions will be exported as the implementations - -- of their respective declared fields in the signature unless overridden - -- by the module implementation. - -- - -- Examples of default implementations: - -- - -- > sig { - -- > Fwip : Type ; - -- > foo : a ; // no default implementation - -- > bar : b = x ; // `bar` defaults to `x` - -- > baz : Thing ; - -- > // `baz` defaults to `cool` only if an instance of `Cool Thing` is in scope - -- > baz : Cool Thing ⇒ Thing = cool ; - -- > } - -- - -- I don't feel like including examples of `open` in signatures - -- because I'm sick of writing docs, so I hope you get the idea - -- based on my wall of text. - -- - -- Finally, this is how visibility works: - -- - -- * All declarations are public; @pub@ modifiers are forbidden - -- because they would be strictly redundant. - -- - -- * All definitions associated with a declaration are public; - -- @pub@ modifiers are allowed but redundant. - -- - -- * Definitions without a declaration are public only if marked @pub@; - -- otherwise, there will be no "inferred declaration". | Sig [Either (NonEmpty Text, Type) TopLevel] deriving Show --- | A pattern matching against a data type's constructors --- or a codata type's eliminators. --- --- A nested pattern is composed of some depth of codata eliminators --- containing some depth of data constructors; --- matching codata eliminators is used to construct codata types, --- whereas matching data constructors is used to eliminate data types. --- --- Patterns are used primarily in the context of 'CaseBranch'es. data Pattern - -- | Bind the matched value to a variable, with an optional type annotation. - -- - -- > foo : bar - -- > foo - -- - -- A variable name may be bound multiple times in the same pattern - -- if and only if the type checker can prove that both - -- uses have identicial values. = PatVar Text (Maybe Type) - -- | An irrelevant pattern completely ignores the matched value. - -- - -- > _ + -- | @_@ | Irrelevant - -- | An impossible pattern matches a value of a type which - -- the typechecker can prove is not possibly inhabited. - -- - -- > ! + -- | @!@ | Impossible - -- | Match against a data constructor or codata eliminator. - -- (See also 'PatAppI'.) - -- - -- > Left x - -- > π₁ xy - -- > Pair x y | PatApp Text [Pattern] - -- | Match against a mixfix data constructor or codata eliminator. - -- (See also 'PatApp'.) - -- - -- The mixfix constructor must be completely applied to patterns. - -- - -- > x ∷ xs // Pattern match against a list constructor. | PatAppI Text (NonEmpty Pattern) - -- | Apply a function to the value and then pattern match against it. - -- This may be used with e.g. copattern eliminators. - -- - -- If the matched value has type @a@, then @( f : a → b ) → ( x : b )@. - -- - -- > π₁ → foo // Pattern match against the left value of an &-pair. - -- - -- This syntax is based on Haskell's view patterns. + -- | @ ← @ | View Expr Pattern | PatLit (Lit Pattern) deriving Show --- | A case branch has a left-hand side which --- consists of some number of patterns to be matched and guards, --- and a right-hand side consisting of an expression. --- In an expression with multiple cases branches, --- each left-hand side has the same type, --- and each right-hand side has the same type (plus copattern matches). --- --- To give a bit of an example, in: --- --- > { --- > pat1 | pat2 → foo ; --- > pat3 | pat4 → bar ; --- > } --- --- `pat1` and `pat3` both match a value of the same type, --- `pat2` and `pat4` both match a value of the same different type, --- and `foo` and `bar` both have yet another different matching type. --- --- In the case of copattern matches, e.g. --- --- > { --- > π₁ → foo ; --- > π₂ → bar ; --- > } --- --- then @foo : a@ and @bar : b@ have different types, --- but the return type of the expression as a whole remains the same: @a & b@. --- --- In every context, the case branch syntax uses 'FlexibleSeparatorSyntax'. --- --- Additionally, if there is only one case branch, --- all of the parentheses and semicolons can usually be elided --- in a context where block syntax is permitted: --- --- > → --- --- The behavior of case branches is yet more complex: see 'Refinement' and 'Guards' --- for the additional things that case branches can do. +-- | @ [| ...]? ? [? → ]?@ data CaseBranch - -- | A branch may introduce additional values to match against using __plus clauses__. - -- This allows /refining/ previous branches, for example by introducing a proof - -- so that two variables may be /unified/ by matching against the identity type, - -- or by proving that a type is uninhabited so that an impossible pattern may be used. - -- - -- For example, when matching against two values @x : Nat@, @y : Nat@ - -- such that @x ~ z × 2@ and @y ~ z + z@, - -- and given a function @p : (z : Nat) → z × 2 ≡ z + z@: - -- - -- > { - -- > // additionally pattern match against the value `p z` - -- > x y + p z - -- > // now that a proof of equality is in-scope, we can refine our match - -- > x x | Refl → ... - -- > } - -- - -- The additional patterns may be matched without modifying the original pattern; - -- in this case, the patterns list will only - -- include the patterns for newly-introduced matches, - -- and the rest of the pattern match can be assumed to be the same. - -- - -- > { - -- > some complex patterns | foo ; - -- > // `...` is identical to writing `some complex patterns`; - -- > // all of the variables that it bound are still in scope. - -- > ... | pat1 → asdasd - -- > ... | pat2 → iouqwe - -- > } - -- - -- This syntax is based on Agda's with clauses. = Refinement [Pattern] [Expr] (NonEmpty CaseBranch) - -- | In addition to pattern matches, branches may be subdivided by 'Guard' clauses, - -- which are conditional expressions. - -- If no guard clause is true, then further case patterns will be tried. - -- (This is different from the behavior of Haskell, which can only match one pattern, - -- and will fail due to non-exhaustive patterns if none of the guards match.) - -- - -- > { - -- > One x ? isGood x → foo ; // if `x` is good - -- > Two y ? isBad y → bar // if `y` is bad - -- > ? else → baz ; // if `y` is /not/ bad - -- > Three z ? isFun z → quux ; // if `z` is fun - -- > _ → floo ; // if `x` is not good /or/ `z` is not fun - -- > } - -- - -- With regards to view patterns and guard fall-through, - -- patterns and guard clauses will always be evaluated top-to-bottom, - -- to the extent that the behavior of the program would be affected - -- by the order of evaluation for guard clauses. - -- - -- This syntax is based on Haskell's guard clauses. + | Guards [Pattern] (NonEmpty (Guard, Expr)) -- | A case branch without refinement or guards. | PlainCase [Pattern] Expr deriving Show --- | A guard is a kind of syntax for conditionals used as part of a 'CaseBranch'. --- --- A guard is a sequence of plain pattern matches (/no/ plus or guard clauses) --- against expressions /or/ expressions with a truth value (e.g. booleans)¹. --- A guard returns true only if all patterns match and all expressions are truthy. --- --- For example: --- --- > ? x ← foo | y ← bar | isNice x && isNaughty y --- --- Or as a simpler example: --- --- > ? isCool foo --- --- ¹: I might add a typeclass for 'truthiness' to allow using guard clause syntax. --- Or it'll just be hardcoded for use by booleans; I'm not sure. type Guard = [Either (Pattern, Expr) Expr] -- | Special syntactic support for a few very important types. @@ -902,35 +234,3 @@ data Lit r -- This uses 'FlexibleSeparatorSyntax'. | LitList [r] deriving Show - --- | When the languages has things within brackets separated by a divider, --- that divider will usually be allowed redundantly both preceding and trailing. --- --- This allows for more flexible layouts, for example with 'CaseBranch': --- --- > { --- > → ; --- > → ; --- > } --- > --- > { --- > ; → --- > ; → --- > } --- > --- > { → --- > ; → --- > } --- --- The benefit of trailing or preceding dividers for multi-line things like this --- is that it allows for uniformity, which looks good, and additionally, --- it means that re-ordering elements is as simple as copy-pasting the --- entire line, without having to add or remove dividers anywhere. --- (Most programmers probably already know about this trick.) --- --- This sort of syntax occurs in many places, e.g.: --- 'ADT', 'GADT', 'Sig', 'Mod', 'CaseBranch', 'Use', and 'Let'. --- --- This data type isn't actually used for anything; --- it's just so that I can link to this explanation in Haddock. -data FlexibleSeparatorSyntax diff --git a/src/Ivo/Syntax/Parser.hs b/src/Ivo/Syntax/Parser.hs index d81c8d6..a59153a 100644 --- a/src/Ivo/Syntax/Parser.hs +++ b/src/Ivo/Syntax/Parser.hs @@ -266,6 +266,7 @@ exTypeApp = label "type application" $ try do -- | 'Lam' with only one undelimited case branch exBlockLam = label "λ expression" $ try do + tkLam args <- many pattern_ tkArr body <- ambiguous @@ -273,6 +274,7 @@ exBlockLam = label "λ expression" $ try do -- | 'Lam' with delimited case branches exFiniteLam = label "λ-case expression" $ try do + tkLam simpleArgs <- many pattern_ body <- caseBranches pure $ Lam simpleArgs body