Lenguaje de Programación para Matemática | Idris

Vista General

Idris es un lenguaje de programación funcional Puro de uso general con tipos dependientes.  Los tipos dependientes  se declaran con losvalores, lo que significa que algunos aspectos del comportamiento de un programa se pueden especificar con precisión en el tipo. Se compila, con la Evaluación perezosa . Sus características están influenciadas por Haskell y ML, e incluyen:

  • Tipos dependientes completos con coincidencia de patrones dependientes
  • Interfaz de función extranjera simple (a C)
  • El compilador permite la edición interactiva: el compilador le ayuda a escribir código usando los tipos.
  • cláusulas WHERE, regla WITH , simples expresiones con CASE, búsqueda de patrones cn LET y los enlaces de lambda
  • Registros dependientes con proyección y actualización
  • Interfaces (similares a clases de tipo en Haskell)
  • Resolución de sobrecarga basada en el tipo
  • DO notación entre paréntesis y las expresiones idiomáticas
  • Sintaxis significativa de sangría
  • Sintaxis extensible
  • Universos acumulativos
  • Comprobación de la totalidad
  • Entorno interactivoañ estilo HUGS

El lenguaje soporta un intetactivo comprobador de Teoremas comparable a Coq , incluyendo tácticas, mientras que este se enfoca en la programación de propósito general que en la prueba teoremas.

Deja un comentario

Tu dirección de correo electrónico no será publicada. Los campos obligatorios están marcados con *