Commit 6955d545 authored by Marcos Viera's avatar Marcos Viera

archivos charla damian

parent c4c4158e
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UnicodeSyntax #-}
{-# LANGUAGE TypeApplications #-}
import Prelude hiding (Show, show)
data CMapKey k mk = CMapKey {cempty v. mk v, clookup v. mk v -> k Maybe v}
aux = \(MapInt m) \k foldr (\(x,v) f if (x == k) then (Just v) else f) Nothing m
data MapInt v = MapInt [(Int,v)]
d1 CMapKey Int MapInt
d1 = CMapKey {cempty = MapInt [], clookup = aux}
-- d₁ = Map Int ⇝ MapInt
data MapPair ma mb v = MapPair (ma (mb v))
d2 ma mb a b. CMapKey a ma CMapKey b mb CMapKey (a,b) (MapPair ma mb)
d2 mai mbi = CMapKey {cempty = MapPair (cempty mai), clookup = \(MapPair m) \(ka,kb) clookup mai m ka >>= (\m clookup mbi m kb)}
-- 3 tipos de entorno
-- Ω : Entorno de definiciones de tipos asociados a declaraciones de instancia
-- Map Int ⇝ MapInt --asociado a la declaración Map Int
-- ∀ a b. Map (a,b) ⇝ MapPair (Map a) (Map b) --asociado a la declaración (Map a, Map b) ⇒ Map (a,b)
-- Map a ⇝ β --asociado a la declaración local Map a ⇒ … en el tipo de una función
--Δ : entorno de diccionarios asociados a declaraciones de instancia
--d₁ : Map Int
--d₂ : ∀ a b. (Map a, Map b) ⇒ Map (a,b)
--Γ : entorno de tipos fuente:
-- (x: σ₁), (y:σ₂)
----------Juicios de transformación de tipos fuente a tipos objeto----------
-----trΩ1-----
-- Ω |- ∀ a b, Map (a,b) ⇝ MapPair (Map a, Map b) Ω |- Map Int ⇝ MapInt, Map α ⇝ β
-- Ω |- Map (Int, Int) ⇝ MapPair MapInt β
--------------
-- Ω |- List ⇝ List Ω |- Map Int ⇝ MapInt
--List (Map Int Int) ⇝ List (MapInt)
-----trπ-----
-- Ω |- MapKey a ⇝ (Map α ⇝ β), CMapKey a β Ω, Map a ⇝ β |- Map (a,Int) ⇝ MapPair β MapInt
-- Ω |- MapKey α ⇒ Map (α, Int) ⇝ ∀ β. CMapKey α β → MapPair (β, MapInt)
----------Juicios de transformación de declaraciones de instancia a tipos objeto----------
-- Ω |- Map Int ⇝ MapInt
-- Ω |- MapKey Int ⇝ MapInt
-- Ω |- Map (α,b) ⇝ MapPair (Map a) (Map b)
-- Ω |- MapKey (a,b) ⇝ MapPair (Map a) (Map b)
----------Juicios de transformación de tipos cualificados a tipos objeto----------
-- Ω |- MapKey a ⇝ β Ω |- a ⇝ a
-- Ω |- MapKey a ⇝ (Map a ⇝ β) , CMapKey a β
-- Ω |- MapKey (a,Int) ⇝ MapPair γ MapInt Ω |- γ ⇝ γ Ω |- MapInt ⇝ MapInt
-- Ω |- MapKey (a,Int) ⇝ (MapPair γ MapInt ⇝ β), CMapKey (a,Int) β
----------Juicios de transformación de declaraciones de instancia a términos----------
-----mono-----
--(d₁: Map Int) ∈ Δ
--Map Int ⇝ d₁
-----spec-----
-- Ω |Δ |- ∀ a b. (MapKey a, MapKey b) ⇒ MapKey (a,b) ⇝ d₂ Ω |- MapKey Int ⇝ MapInt
-- Ω |- (MapKey Int, MapKey Int) ⇒ MapKey (Int,Int) ⇝ d₂
--no estamos saliendonos del esquema sináctico para las declaraciones de instancia??
-----mp-----
-- Ω |Δ |- (MapKey Int, MapKey Int) ⇒ MapKey (Int,Int) ⇝ d₂ Ω | Δ |- MapKey Int ⇝ d₁ Ω |- MapKey Int ⇝ MapInt
-- Ω |- MapKey (Int, Int) ⇝ d₂ d₁ d₁
d3 = d2 @MapInt @MapInt d1 d1 CMapKey (Int,Int) (MapPair MapInt MapInt)
---------------------------------------------------------------------------------------------------
---------- Juicios de tranducción de términos----------
-- Ω|Δ|Γ |- e ⇝ w': σ donde e es el término fuente, w' el término objeto y σ el tipo fuente
-----(⇒ E)-----
-- Ω |Δ | Γ |- (cempty ∷ ⇝ cempty : MapKey Int ⇒ Map Int Ω | Δ ||- MapKey Int ⇝ d₁ Ω |- MapKey Int ⇝ MapInt
-- Ω |Δ | Γ |- cempty d₁ : Map Int
--Los ∀ explicitos son para pasar a System F no?
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UnicodeSyntax #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
------------------------------Section 1-------------------------------
import Prelude hiding (Show, head, show, Map, empty, lookup)
import Control.Monad.State
class MapKey k where
data Map k v
empty :: Map k v
lookup Map k v k Maybe v
aux m k = foldr (\(x,v) f if (x == k) then (Just v) else f) (Nothing) m
instance MapKey Int where
data Map Int v = IntMap [(Int,v)]
empty = IntMap []
lookup (IntMap m) = aux m
-- :t intMapKeyInstance
instance (MapKey a, MapKey b) MapKey (a,b) where
data Map (a,b) v = PairMap (Map a (Map b v))
empty = PairMap empty
lookup (PairMap m) (a,b) = (lookup m a) >>= (\m lookup m b)
instance (MapKey a) MapKey [a] where
data Map [a] v = ListMap (Maybe v) (Map a (Map [a] v))
empty = ListMap Nothing empty
lookup (ListMap mv _) [] = mv
lookup (ListMap _ m) (x:xs) = lookup m x >>= \map lookup map xs
--f ∷ MapKey a ⇒ Map (a,Int) v → a → Maybe v
--f m k = lookup m (k,42)
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UnicodeSyntax #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
------------------------------Section 1-------------------------------
import Prelude hiding (Show, head, show, Map, empty, lookup)
import Control.Monad.State
class MapKey k where
data Map k v
empty :: Map k v
lookup Map k v k Maybe v
instance MapKey Int where
data Map Int v = IntMap [(Int,v)]
empty = IntMap []
lookup (IntMap m) = \k -> foldr (\(x,v) f if (x == k) then (Just v) else f) (Nothing) m
instance (MapKey a, MapKey b) MapKey (a,b) where
data Map (a,b) v = PairMap (Map a (Map b v))
empty = PairMap empty
lookup (PairMap m) (a,b) = (lookup m a) >>= (\m lookup m b)
f MapKey a Map (a,Int) v a Maybe v
f m k = lookup m (k,42)
instance (MapKey a) MapKey [a] where
data Map [a] v = ListMap (Maybe v) (Map a (Map [a] v))
empty = ListMap Nothing empty
lookup (ListMap mv _) [] = mv
lookup (ListMap _ m) (x:xs) = lookup m x >>= \map lookup map xs
example = lookup (ListMap (Just 2) (IntMap [(1, ListMap (Just 1) empty)])) [1]
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UnicodeSyntax #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
import Prelude hiding (lookup,empty)
import Data.Function
data CMapKey k mk = CMapKey {empty v. mk v, lookup v. mk v k Maybe v}
dint = CMapKey {empty = IntMap [],
lookup = \(IntMap m) \k foldr (\(x,v) f
if (x == k) then (Just v) else f) (Nothing) m}
data IntMap v = IntMap [(Int,v)]
data PairMap ma mb v = PairMap (ma (mb v))
dpair :: CMapKey a ma CMapKey b mb CMapKey (a,b) (PairMap ma mb)
dpair mae mbe =CMapKey {empty = PairMap (empty mae),
lookup = \(PairMap m) \(ka,kb) ((lookup mae m ka) >>= (\m lookup mbe m kb))}
f CMapKey a ma (PairMap ma IntMap v) a Maybe v
f d m ka = lookup (dpair d dint) m (ka,1)
data ListMap ma v = ListMap (Maybe v) (ma (ListMap ma v))
dlist CMapKey a ma CMapKey [a] (ListMap ma)
dlist da = CMapKey {empty = ListMap Nothing (empty da),
lookup = fix (\r
\(ListMap mv m)
\l case l of
[] mv
(x:xs) (lookup da m x) >>= \map (r map xs))}
dlistint = dlist dint
example = lookup dlistint (ListMap (Just 2) (IntMap [(1, ListMap (Just 1) (empty dint))])) [1]
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment