scala - valores, tipos, tipos,... como una secuencia infinita?

haskell functional-programming

Question

Solo comienzo a familiarizarme con el concepto de tipos, así que tengan paciencia si no estoy formulando bien mis preguntas ...

Los valores tienen tipos:

3 :: Int
[1,2,3] :: [Int]
(''c'',True) :: (Char,Bool)

Tipos tienen tipos:

the type ''Int'' has kind *
the type ''[Int]'' also has kind *
   but the type constructor [] has kind * -> *
similarly, the type (Char,Bool) has kind  *
   but the type constructor (,) has kind * -> * -> *

¿Qué tienen los tipos?

¿Tienen los tipos el tipo, los géneros, las razas o las variedades?

¿Hasta dónde va esta secuencia de abstracción? ¿Nos detenemos porque nos quedamos sin palabras, o nos detenemos porque ir más lejos no tiene ningún valor? ¿O, quizás, porque alcanzamos rápidamente los límites de la cognición humana y simplemente no podemos guiarnos por tipos de géneros más elevados?

Una pregunta relacionada: los idiomas nos dan constructores de valores (como un operador contra) para hacer valores. Los idiomas también nos dan constructores de tipos como (,) o [] para hacer tipos. ¿Hay algún lenguaje que exponga a los constructores de clases para hacer tipos?

Otro caso marginal sobre el que tengo curiosidad: aparentemente tenemos un tipo que no tiene ningún valor, denotado como ⊥, llamado "el tipo de fondo". ¿Hay algún tipo que no tenga tipo: un tipo inferior?

Answer 1

El type y type terminología no se escala bien. Escriba teóricos ya que Bertrand Russell ha usado una jerarquía de "tipos". Una versión de esto tiene ese Integer : Type 0, Type 0 : Type 1, Type 1 : Type 2, ..., Type n : Type (n+1), .... En idiomas de Integer : Type 0, Type 0 : Type 1, Type 1 : Type 2, ..., Type n : Type (n+1), .... dependientes como Coq y Agda, uno frecuentemente necesita estos "tipos superiores".

Niveles como este son útiles para evitar la paradoja de Russell . Usar Type : Type tiende a causar contradicción (ver Quine para diseños alternativos).

Este uso de números es la notación estándar cuando lo necesitamos. Algunas teorías de tipo tienen una noción de "tipos acumulativos", "niveles acumulativos" o "géneros acumulativos" que dice "si t : Type n y también t : Type (n+1) ".

Los niveles acumulativos + "polimorfismo de nivel" dan una teoría casi tan flexible como Type : Type , pero evita las paradojas. Coq hace que los niveles estén implícitos en su mayoría, aunque los géneros Set y Prop se escriben Type , Type {1} : Type {2} . Es decir, normalmente no ves los números, y la mayoría de las veces simplemente funciona.

Agda tiene un pragma de lenguaje que proporciona polimorfismo de nivel y hace que las cosas sean muy flexibles, pero puede ser ligeramente burocrático (sin embargo, Agda suele ser menos "burocrático" que Coq en otras áreas).

Otra buena palabra es "universo".

Answer 2

Probablemente deberías leer el artículo de Tim Sheard sobre Omega, un dialecto de Haskell con una infinidad de tipos / clases / tipos, pero sin tipos dependientes en toda regla. Explica por qué querría esto, y menciona que los niveles anteriores de "clasificación" están en práctica (al menos hasta ahora) y no se usan mucho en forma directa.