Misplaced Pages

#176823

38-520: Agda may refer to: Agda (programming language) , the programming language and theorem prover Agda (Golgafrinchan) , the character in The Hitchhiker's Guide to the Galaxy by Douglas Adams Liten Agda , the heroine of a Swedish legend Agda Montelius , a Swedish feminist Agda Persdotter , a Swedish royal mistress of the 16th-century Agda Rössel ,

76-481: A Haskell -like syntax . The system has Emacs , Atom , and VS Code interfaces but can also be run in batch processing mode from a command-line interface . Agda is based on Zhaohui Luo's unified theory of dependent types (UTT), a type theory similar to Martin-Löf type theory . Agda is named after the Swedish song "Hönan Agda", written by Cornelis Vreeswijk , which is about a hen named Agda. This alludes to

114-584: A Swedish politician Agda Östlund , a Swedish politician Dayan Agda, a Filipino politician Topics referred to by the same term [REDACTED] This disambiguation page lists articles associated with the title Agda . If an internal link led you here, you may wish to change the link to point directly to the intended article. Retrieved from " https://en.wikipedia.org/w/index.php?title=Agda&oldid=1171742137 " Categories : Disambiguation pages Disambiguation pages with given-name-holder lists Hidden categories: Short description

152-465: A constructor could carry no data (e.g., Empty ), or one piece of data (e.g., Leaf has one Int value), or multiple pieces of data (e.g., Node has two Tree values). To do something with a value of this Tree algebraic data type, it is deconstructed using a process called pattern matching . This involves matching the data with a series of patterns . The example function depth above pattern-matches its argument with three patterns. When

190-438: A function taking an abstract expression as input and returning an optimized form. Algebraic data types are used to represent values that can be one of several types of things . Each type of thing is associated with an identifier called a constructor , which can be considered a tag for that kind of data. Each constructor can carry with it a different type of data. For example, considering the binary Tree example shown above,

228-574: A lot of tedious and repetitive proofs. Although Agda has no separate tactics language, it is possible to program useful tactics within Agda. Typically, this works by writing an Agda function that optionally returns a proof of some property of interest. A tactic is then constructed by running this function at type-checking time, for example using the following auxiliary definitions: Given a function check-even : (n : N {\displaystyle \mathbb {N} } ) → Maybe (Even n) that inputs

266-458: A natural number. To begin, zero is a natural number, and if n is a natural number, then suc n , standing for the successor of n , is a natural number too. Here is a definition of the "less than or equal" relation between two natural numbers: The first constructor, z≤n , corresponds to the axiom that zero is less than or equal to any natural number. The second constructor, s≤s , corresponds to an inference rule, allowing to turn

304-435: A number and optionally returns a proof of its evenness, a tactic can then be constructed as follows: The actual proof of each lemma will be automatically constructed at type-checking time. If the tactic fails, type-checking will fail. Further, to write more complex tactics, Agda supports automation via reflective programming (reflection). The reflection mechanism allows quoting program fragments into, or unquoting them from,

342-468: A possible more complex recursive pattern would be something like: Node ( Node ( Leaf 4 ) x ) ( Node y ( Node Empty z )) Recursive patterns several layers deep are used for example in balancing red–black trees , which involve cases that require looking at colors several layers deep. The example above is operationally equivalent to the following pseudocode : The advantages of algebraic data types can be highlighted by comparison of

380-451: A product type typically contain several values, called fields . All values of that type have the same combination of field types. The set of all possible values of a product type is the set-theoretic product, i.e., the Cartesian product , of the sets of all possible values of its field types. The values of a sum type are typically grouped into several classes, called variants . A value of

418-448: A proof of n ≤ m into a proof of suc n ≤ suc m . So the value s≤s {zero} {suc zero} (z≤n {suc zero}) is a proof that one (the successor of zero), is less than or equal to two (the successor of one). The parameters provided in curly brackets may be omitted if they can be inferred. In core type theory, induction and recursion principles are used to prove theorems about inductive types . In Agda, dependently typed pattern matching

SECTION 10

#1733093241177

456-403: A safe way for traditional record data structures. However, in pattern matching such problems are not faced. The type of each extracted value is based on the types declared by the relevant constructor. The number of values that can be extracted is known based on the constructor. Secondly, in pattern matching, the compiler performs exhaustiveness checking to ensure all cases are handled. If one of

494-430: A slightly different form, thus: μ ϕ . λ α .1 + α × ϕ   α {\displaystyle \mu \phi .\lambda \alpha .1+\alpha \times \phi \ \alpha } . (Note how the μ {\displaystyle \mu } and λ {\displaystyle \lambda } constructs are reversed relative to

532-463: A slightly more complex example, binary trees may be implemented in Haskell as follows: or Here, Empty represents an empty tree, Leaf represents a leaf node, and Node organizes the data into branches. In most languages that support algebraic data types, it is possible to define parametric types. Examples are given later in this article. Somewhat similar to a function, a data constructor

570-405: A variant type is usually created with a quasi-functional entity called a constructor . Each variant has its own constructor, which takes a specified number of arguments with specified types. The set of all possible values of a sum type is the set-theoretic sum, i.e., the disjoint union , of the sets of all possible values of its variants. Enumerated types are a special case of sum types in which

608-457: Is a full rewrite, which should be considered a new language that shares a name and tradition. Agda is also a proof assistant based on the propositions-as-types paradigm ( Curry–Howard correspondence ), but unlike Coq , has no separate tactics language, and proofs are written in a functional programming style. The language has ordinary programming constructs such as data types , pattern matching , records , let expressions and modules, and

646-490: Is applied to arguments of an appropriate type, yielding an instance of the data type to which the type constructor belongs. For example, the data constructor Leaf is logically a function Int -> Tree , meaning that giving an integer as an argument to Leaf produces a value of the type Tree . As Node takes two arguments of the type Tree itself, the datatype is recursive . Operations on algebraic data types can be defined by using pattern matching to retrieve

684-457: Is different from Wikidata All article disambiguation pages All disambiguation pages Agda (programming language) Agda is a dependently typed functional programming language originally developed by Ulf Norell at Chalmers University of Technology with implementation described in his PhD thesis. The original Agda system was developed at Chalmers by Catarina Coquand in 1999. The current version, originally named Agda 2,

722-527: Is heavy reliance on metavariables for program construction. For example, one can write functions like this in Agda: ? here is a metavariable. When interacting with the system in emacs mode, it will show the user expected type and allow them to refine the metavariable, i.e., to replace it with more detailed code. This feature allows incremental program construction in a way similar to tactics-based proof assistants such as Coq. Programming in pure type theory involves

760-533: Is in beta, and is under active development. One of the more notable features of Agda is a heavy reliance on Unicode in program source code. The standard emacs mode uses shortcuts for input, such as \Sigma for Σ. There are two compiler backends, MAlonzo for Haskell and one for JavaScript . Algebraic data type Two common classes of algebraic types are product types (i.e., tuples and records ) and sum types (i.e., tagged or disjoint unions , coproduct types or variant types ). The values of

798-453: Is like a Greek f .) The function must also now be applied ϕ {\displaystyle \phi } to its argument type α {\displaystyle \alpha } in the body of the type. For the purposes of the List example, these two formulations are not significantly different; but the second form allows expressing so-called nested data types , i.e., those where

SECTION 20

#1733093241177

836-400: Is only one constructor, the data type is a product type. Further, the parameter types of a constructor are the factors of the product type. A parameterless constructor corresponds to the empty product . If a datatype is recursive, the entire sum of products is wrapped in a recursive type , and each constructor also rolls the datatype into the recursive type. For example, the Haskell datatype:

874-902: Is represented in type theory as λ α . μ β .1 + α × β {\displaystyle \lambda \alpha .\mu \beta .1+\alpha \times \beta } with constructors n i l α = r o l l   ( i n l   ⟨ ⟩ ) {\displaystyle \mathrm {nil} _{\alpha }=\mathrm {roll} \ (\mathrm {inl} \ \langle \rangle )} and c o n s α   x   l = r o l l   ( i n r   ⟨ x , l ⟩ ) {\displaystyle \mathrm {cons} _{\alpha }\ x\ l=\mathrm {roll} \ (\mathrm {inr} \ \langle x,l\rangle )} . The Haskell List datatype can also be represented in type theory in

912-431: Is similar (to extract parts from a piece of data matching certain constraints) however, the implementation is very different. Pattern matching on algebraic data types matches on the structural properties of an object rather than on the character sequence of strings. A general algebraic data type is a possibly recursive sum type of product types . Each constructor tags a product type to separate it from others, or if there

950-465: Is used instead. For example, natural number addition can be defined like this: This way of writing recursive functions/inductive proofs is more natural than applying raw induction principles. In Agda, dependently typed pattern matching is a primitive of the language; the core language lacks the induction/recursion principles that pattern matching translates to. One of the distinctive features of Agda, when compared with other similar systems such as Coq ,

988-495: The abstract syntax tree . The way reflection is used is similar to the way Template Haskell works. Another mechanism for proof automation is proof search action in Emacs mode. It enumerates possible proof terms (limited to 5 seconds), and if one of the terms fits the specification, it will be put in the meta variable where the action is invoked. This action accepts hints, e.g., which theorems and from which modules can be used, whether

1026-406: The above pseudocode with a pattern matching equivalent. Firstly, there is type safety . In the pseudocode example above, programmer diligence is required to not access field2 when the constructor is a Leaf . Also, the type of field1 is different for Leaf and Node . For Leaf it is Int but for Node it is Tree . The type system would have difficulties assigning a static type in

1064-635: The action can use pattern matching, etc. Agda is a total functional programming language, i.e., each program in it must terminate and all possible patterns must be matched. Without this feature, the logic behind the language becomes inconsistent, and it becomes possible to prove arbitrary statements. For termination checking , Agda uses the approach of the Foetus termination checker. Agda has an extensive de facto standard library , which includes many useful definitions and theorems about basic data structures, such as natural numbers, lists, and vectors. The library

1102-520: The arguments. For example, consider a function to find the depth of a Tree , given here in Haskell: Thus, a Tree given to depth can be constructed using any of Empty , Leaf , or Node and must be matched for any of them respectively to deal with all cases. In case of Node , the pattern extracts the subtrees l and r for further processing. Algebraic data types are highly suited to implementing abstract syntax . For example,

1140-646: The cases of the depth function above were missing, the compiler would issue a warning. Exhaustiveness checking may seem easy for simple patterns, but with many complex recursive patterns, the task soon becomes difficult for the average human (or compiler, if it must check arbitrary nested if-else constructs). Similarly, there may be patterns which never match (i.e., are already covered by prior patterns). The compiler can also check and issue warnings for these, as they may indicate an error in reasoning. Algebraic data type pattern matching should not be confused with regular expression string pattern matching. The purpose of both

1178-463: The constructor Leaf . Patterns are recursive, so then the data that is associated with that constructor is matched with the pattern "n". In this case, a lowercase identifier represents a pattern that matches any value, which then is bound to a variable of that name — in this case, a variable “ n ” is bound to the integer value stored in the data type — to be used in the expression to evaluate. The recursion in patterns in this example are trivial, but

Agda - Misplaced Pages Continue

1216-506: The constructors take no arguments, as exactly one value is defined for each constructor. Values of algebraic types are analyzed with pattern matching , which identifies a value by its constructor or field names and extracts the data it contains. Algebraic data types were introduced in Hope , a small functional programming language developed in the 1970s at the University of Edinburgh . One of

1254-426: The following algebraic data type describes a simple language representing numerical expressions: An element of such a data type would have a form such as Mult (Add (Number 4) (Minus (Number 0) (Number 1))) (Number 2) . Writing an evaluation function for this language is a simple exercise; however, more complex transformations also become feasible. For example, an optimization pass in a compiler might be written as

1292-407: The function is called, it finds the first pattern that matches its argument, performs any variable bindings that are found in the pattern, and evaluates the expression corresponding to the pattern. Each pattern above has a form that resembles the structure of some possible value of this datatype. The first pattern simply matches values of the constructor Empty . The second pattern matches values of

1330-836: The most common examples of an algebraic data type is the singly linked list . A list type is a sum type with two variants, Nil for an empty list and Cons x xs for the combination of a new element x with a list xs to create a new list. Here is an example of how a singly linked list would be declared in Haskell : or Cons is an abbreviation of cons truct. Many languages have special syntax for lists defined in this way. For example, Haskell and ML use [] for Nil , : or :: for Cons , respectively, and square brackets for entire lists. So Cons 1 (Cons 2 (Cons 3 Nil)) would normally be written as 1:2:3:[] or [1,2,3] in Haskell, or as 1::2::3::[] or [1,2,3] in ML. For

1368-503: The name of the theorem prover Coq , which was named after Thierry Coquand . The main way of defining data types in Agda is via inductive data types which are similar to algebraic data types in non-dependently typed programming languages. Here is a definition of Peano numbers in Agda: Basically, it means that there are two ways to construct a value of type N {\displaystyle \mathbb {N} } , representing

1406-411: The original.) The original formation specified a type function whose body was a recursive type. The revised version specifies a recursive function on types. (The type variable ϕ {\displaystyle \phi } is used to suggest a function rather than a base type like β {\displaystyle \beta } , since ϕ {\displaystyle \phi }

1444-486: The recursive type differs parametrically from the original. (For more information on nested data types, see the works of Richard Bird , Lambert Meertens , and Ross Paterson.) In set theory the equivalent of a sum type is a disjoint union , a set whose elements are pairs consisting of a tag (equivalent to a constructor) and an object of a type corresponding to the tag (equivalent to the constructor arguments). Many programming languages incorporate algebraic data types as

#176823