On 3 June 2015 at 01:32, Keean Schupke <ke...@fry-it.com> wrote: > I have gone for including a solver in the compiler. The solver is (at the > moment) a kind of improved Prolog, and theorems to prove, as well as hints > can be included with the source. > > What is interesting about this approach is that many type system things > can be expressed in the logic language without special support in the > actual language. Examples of this are type classes and type families, which > can be expressed as logic and overloaded functions. > > Keean. > ​Concur.
The popular way to do this is to have a logic language or a pattern-matching functional language and a way to compute with the terms and types of the language. Coq and Idris have both, and that language is about 7000 lines for Idris, including type provider and typeclass support. So, all that needs to be specified is a small language and a way to map types in the dynamics language to values in the statics language, and then anything further can be distributed as a library in the statics. -- William Leslie Notice: Likely much of this email is, by the nature of copyright, covered under copyright law. You absolutely MAY reproduce any part of it in accordance with the copyright law of the nation you are reading this in. Any attempt to DENY YOU THOSE RIGHTS would be illegal without prior contractual agreement.
_______________________________________________ bitc-dev mailing list bitc-dev@coyotos.org http://www.coyotos.org/mailman/listinfo/bitc-dev
