1votos

Máquina de Turing en el sistema de tipos en Haskell

por josejuan hace 5 años

Usando Peano, se suma, se multiplica (por 10) y se obtienen las paridades en tiempo de compilación.

Animado por la elegante solución de @jmgomez al desafío Cálculo número primo con expresiones lambda, propongo realizar algún tipo de computación usando únicamente el sistema de tipos. Lógicamente, la computación debe resolverse en tiempo de compilación, nunca en tiempo de ejecución.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
{-# LANGUAGE FlexibleInstances, FlexibleContexts, UndecidableInstances, MultiParamTypeClasses, FunctionalDependencies #-} 
 
-- El propio compilador necesitará de un tamaño considerable al usar los axiomas de Peano de forma explícita 
-- ghci -fcontext-stack=1000 
 
-- Ocultamos para poder usar los mismo nombres 
import Prelude hiding (even, pred, succ, odd) 
 
-- Ninguna computación se hará en tiempo de ejecución, es más, todos los valores quedan "undefined", por lo que, 
-- de usarse en tiempo de ejecución, producirá una excepción (de "undefined") 
u = undefined 
 
-- Los números naturales (y el cero) pueden quedar expresados como el cero y sus sucesores 
data Zero 
data Succ n 
 
-- Una computación que definimos es la paridad, en este caso saber si es Par 
class Even x 
 
-- El cero es Par 
instance Even Zero 
 
-- Cualquier otro, deberá ser el sucesor del sucesor de otro Par anterior 
instance Even a => Even (Succ (Succ a)) 
 
-- Por comodidad, podemos definir constructores para comprobar la paridad *DE LOS TIPOS* (los valores *NO SE USAN*) 
even :: Even a =>      a -> Bool; even _ = True 
odd  :: Even a => Succ a -> Bool; odd  _ = True 
 
-- Otra computación, puede ser la suma, que se hace estableciendo la identidad A + B = C mediante tipos 
class Add a b ab | a b -> ab, a ab -> b 
instance Add Zero b b 
instance (Add a b ab) => Add (Succ a) b (Succ ab) 
 
-- Por comodidad también, definimos un constructor que hace la suma de tipos 
add :: Add a b c => a -> b -> c; add _ _ = u 
 
-- Otra computación, puede ser multiplicar por 10, que sólo es sumar 10 veces una cantidad ¡¡el cómputo se hace en tiempo de compilación!! 
byten x = add x $ add x $ add x $ add x $ add x $ add x $ add x $ add x $ add x x 
 
-- Por comodidad, podemos definir un constructor de números naturales, aportando 3 dígitos (ej. 001, 302, ...) 
nat a b c = add c $ byten $ add b $ byten a 
 
-- Por comodidad, podemos definir un constructor para cada dígito 
_0 :: Zero; _0 = u 
_1 :: Succ Zero; _1 = u 
_2 :: Succ (Succ Zero); _2 = u 
_3 :: Succ (Succ (Succ Zero)); _3 = u 
_4 :: Succ (Succ (Succ (Succ Zero))); _4 = u 
_5 :: Succ (Succ (Succ (Succ (Succ Zero)))); _5 = u 
_6 :: Succ (Succ (Succ (Succ (Succ (Succ Zero))))); _6 = u 
_7 :: Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))); _7 = u 
_8 :: Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))); _8 = u 
_9 :: Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))); _9 = u 
 
-- Por comodidad, podemos visualizar los números generados, convirtiéndolos en números enteros 
class Nat a where 
  toInt :: a -> Int 
 
instance Nat Zero where 
  toInt   _ = 0 
 
instance Nat x => Nat (Succ x) where 
  toInt x = toInt (pred x) + 1 
            where pred :: Succ x -> x 
                  pred _ = u 
 
 
 
{- 
 
-- Así, podemos hacer computaciones que son resueltas en tiempo de compilación (¡ojo!, la optimización final 
-- de las operaciones realizadas dependerá de lo bueno o malo que sea el compilador, por ejemplo, una vez 
-- definida la suma de dos números mediante los tipos, la función `byten` queda definida como un conjunto de 
-- operaciones sobre *constantes* pero eso no quiere decir que el compilador las optimice [aunque es muy probable 
-- que sí y que quede el valor final]). 
 
-- Ejempo de visualizar un número representado mediante tipos 
*Main> toInt $ nat _3 _0 _1 
301 
 
-- Un ejemplo de la validación en tiempo de compilación de un número impar 
*Main> odd $ nat _3 _0 _1 
True 
 
-- Un ejemplo de la validación en tiempo de compilación de un número par 
*Main> even $ nat _3 _0 _2 
True 
 
-- Un ejemplo del error en tiempo de compilación de que el número no es par 
*Main> even $ nat _3 _0 _1 
 
<interactive>:26:1: 
    No instance for (Even (Succ Zero)) arising from a use of `even' 
    Possible fix: add an instance declaration for (Even (Succ Zero)) 
    In the expression: even 
    In the expression: even $ nat _3 _0 _1 
    In an equation for `it': it = even $ nat _3 _0 _1 
*Main> odd $ nat _3 _0 _2 
 
-- Un ejemplo del error en tiempo de compilación de que el número no es impar 
<interactive>:27:1: 
    No instance for (Even (Succ Zero)) arising from a use of `odd' 
    Possible fix: add an instance declaration for (Even (Succ Zero)) 
    In the expression: odd 
    In the expression: odd $ nat _3 _0 _2 
    In an equation for `it': it = odd $ nat _3 _0 _2 
 
-- Un ejemplo de una operación ( 301 + 10 * 57 ) realizada en tiempo de compilación 
*Main> toInt $ add (nat _3 _0 _1) $ byten (nat _0 _5 _7) 
871 
 
 
 
 
-- Para verificar que no se hace en tiempo de ejecución, podemos compilar lo siguiente 
 
main = print $ toInt $ add (nat _3 _0 _1) $ byten (nat _0 _5 _7) 
 
-- Que le cuesta bastante (como 60segundos) obtener el ejecutable al hacer 
D:\Projects\haskell>ghc -O3 nat.hs -fcontext-stack=2000 
[1 of 1] Compiling Main             ( nat.hs, nat.o ) 
Linking nat.exe ... 
 
 
-- Pero cuya ejecución es inmediata 
D:\Projects\haskell>nat.exe 
871 
 
-} 
7 comentarios
0votos

Escrito por jmgomez hace 5 años

¡Muy buena!

En F*, como sabes, restringir el dominio es trivial, e.g. para que solo admita impares menores de 100:

type even = n:int { n % 2 <> 0 /\ 100 }+

Sin embargo no veo como hacer aritmética con los tipos y menos poder probarlo...
0votos

Escrito por josejuan hace 5 años

En F* no se como se haría, pero en principio no debería haber problema, lo que he mirado por ahí se centra en asegurar invariantes (in/out en las funciones), pero su sistema de tipos es dependiente (vaya, que se pueden crear constructores de tipo con soporte a la inferencia) por lo que debería poderse.

También he mirado de hacerlo con type providers en F#, de hacerlo, creo que debería hacerse con los erasing type providers, para que pueda procesar cualquier nº de forma eficiente, pero está bastante "cutre" (requiere estar al día y dedicar un rato) el tema para crear proveedores de tipos, así que te lo dejo para ti XD XD ;P

Sino, podemos preguntarle a Mauricio.

(digo cutre porque lo que he visto se basa más en un hack que en el soporte del lenguaje, la verdad, creí que estaba mejor la cosa; ahora no veo tan mal el template de haskell [y es feo de narices] ahí ahí andan; tampoco he mirado mucho F# ¿algún tutorial para hacer type providers que funcione? :D :D)
0votos

Escrito por jmgomez hace 5 años

"creo que debería hacerse con los erasing type providers"
No he hecho ninguno, llevo un tiempo con ganas, ésta parece una buena excusa :P Pero, desde la ignorancia, ¿por qué sugieres erasing frente a generative? ¿Por restricciones de tu ejercicio?

"algún tutorial"
No te puedo decir porque no he probado ninguno xD Pero parece que la mayoría se centran en generativos. Los cuales a simple vista parecen más interesantes por el hecho de que se pueden consumir desde CSharp.

En fin, a ver si me animo luego y levanto la máquina virtual (lo más pereza que da xD) y le doy un intento, porque imagino que desde mono el soporte para la creación será tirando a nulo...
0votos

Escrito por josejuan hace 5 años

"¿por qué sugieres erasing frente a generative?"

pues no estoy muy seguro ahora que lo dices, si el azúcar de generative admite escribir algo como
let ... 3 * prime<37>


no veo problema, pero si hay que declarar primero el tipo, el generative no "valdría"

¡Ánimo y salimos de dudas! XD XD
0votos

Escrito por jmgomez hace 5 años

Bueno, estuve hackeando un poco estos samples (no he mirado "teoría") y bueno, pseudo definí los 50 primeros números pares (más por probar que por otra cosa) en un TP generativo y los pude consumir desde CSharp.

A ver si pronto le puedo dedicar más tiempo, la verdad es que mola muuucho ;)

Aquí una prueba :P
0votos

Escrito por josejuan hace 5 años

A eso me refería, no puedes generar todos los nºs primos, de ahí que habrá que crear un nuevo tipo para cada primo a validar; que si queda bien el azúcar no hay mayor inconveniente.

Ya tengo ganas de ver que tal queda ;)

(¡Como mola el screencast! :D)

Comenta la solución

Tienes que identificarte para poder publicar tu comentario.