Add preliminary support for inductive families #133
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This is roughly based on Abel & Cockx's paper (http://www2.tcs.ifi.lmu.de/~abel/lhs-checking-submitted.pdf). It's enough to implement as data types some simple things like propositional equality, finite sets, and vectors, but there's some stuff that still doesn't work very well or is missing, notably: * Coverage and redundancy checks are incomplete. * Error messages are bad. * Dot patterns are missing. Data type indices are desugared in the following way: ``` type Equals a b where Refl : Equals a a ``` becomes ``` type Equals a b where Refl : Builtin.Equals a b => Equals a b ``` We can see that a `Builtin.Equals` (which is distinct from `Equals`, the type being defined in the example) constraint has been inserted for the second parameter of the `Refl` constructor because its type differs from the type definition's head. This makes `Equals` an ordinary parameterised data type again, leaving the job of constraining indices to `Builtin.Equals`. `Builtin.Equals` is a constraint that's special-cased in the compiler. If it occurs in a pattern, it's automatically matched using the SplitEq rule from the aforementioned paper. If the constraint occurs unsolved in an expression, its two arguments are unified and the constraint is solved with `Builtin.Refl` (its lone constructor) as the solution.
This was referenced Feb 21, 2019
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is roughly based on Abel & Cockx's paper
(http://www2.tcs.ifi.lmu.de/~abel/lhs-checking-submitted.pdf).
It's enough to implement as data types some simple things like
propositional equality, finite sets, and vectors, but there's some stuff
that still doesn't work very well or is missing, notably:
Data type indices are desugared in the following way:
becomes
We can see that a
Builtin.Equals(which is distinct fromEquals, thetype being defined in the example) constraint has been inserted for the
second parameter of the
Reflconstructor because its type differs fromthe type definition's head. This makes
Equalsan ordinaryparameterised data type again, leaving the job of constraining indices
to
Builtin.Equals.Builtin.Equalsis a constraint that's special-cased in the compiler.If it occurs in a pattern, it's automatically matched using the SplitEq
rule from the aforementioned paper. If the constraint occurs unsolved in
an expression, its two arguments are unified and the constraint is
solved with
Builtin.Refl(its lone constructor) as the solution.