Convers˜ao de Código Pointwise para Código Point-free
Contents
1. 1 m obt m se fConsty pfeii pfern out Pots pfem1 Pfem nm 00 Novamente se est perante um caso onde poss vel aplicar a mesma lei obtendo se desta vez f pfesi Vo out NE ce N A out Generalizando a situac o para a composic o de mais do que dois construtores desde que agrupando os ramos correctamente e indo eliminando os construtores mais direita nas composi es do lado esquerdo torna se j trat vel a convers o para point free de uma vastid o de casos Os nicos casos que ainda levantam problemas s o aqueles em que existem produtos no lado esquerdo Veja se o caso ap s a elimina o de vari veis f ConstA x ConstB pfen f ConstA x ConstB2 pfe12 f ConstA x ConstB pfein f ConstAm x ConstB pfema f ConstAm x ConstB2 pfem 2 f ConstAm x ConstB pfemn com ConstA com i 1 m todos os construtores de um tipo de dados indutivo ConstB com j 1 n todos os construtores de outro tipo de dados indutivo nada impede que sejam ambos o mesmo e pfe express es point free para i j 1 m x 1 m A partida pensar se ia que um either dos lados direitos com a devida associatividade e o produto das fun es out resolveria o problema Mas out x out retorna um produto de co produtos provavelmente co produtos de aridades diferentes e os eithers dos lados direitos esperariam eithers de pares Pretende se portanto con2. es de inst ncias de classes representam se com o construtor HsInstDecl cuja assinatura HsInstDecl SrcLoc gt HsContext gt HsQName gt HsType gt HsDecl gt HsDecl O terceiro argumento o nome da classe para a qual se destina a inst ncia o quarto argumento a lista de tipos para os quais se cria a inst ncia a lista n o significa que se est o a criar inst ncias para cada um dos tipos listados mas serve para acomodar as classes multi par metro e o quinto argumento a lista com as declara es para a inst ncia tipicamente as nicas declara es que aqui se encontram s o as assinaturas de tipo e as defini es das fun es da classe Syntax 4 3 Fun o Relativamente s defini es de fun es estas s o representadas pelo construtor HsFunBind que tem um nico argumento que uma lista de HsMatch Este ltimo tipo tem um s construtor com o mesmo nome que o tipo HsMatch com a assinatura de tipo que se segue HsMatch SrcLoc gt HsName gt HsPat gt HsRhs gt HsDecl gt HsMatch O segundo argumento o nome da fun o o terceiro a lista de argumentos estes ar gumentos est o num n vel diferente pois s o os argumentos representados havendo lugar a pattern matching o quarto argumento corresponde defini o propriamente dita vul garmente designada lado direito e o quinto argumento uma lista de sub declara es que s o locais defini o actu
3. Convers o de C digo Pointwise para C digo Point free Jos Miguel Vila a jmvilaca di uminho pt Techn Report DI PURe 04 11 02 2004 Novembro PURe Program Understanding and Re engineering Calculi and Applications Project POSI ICHS 44304 2002 Departamento de Inform tica da Universidade do Minho Campus de Gualtar Braga Portugal DI PURe 04 11 02 Convers o de C digo Pointwise para C digo Point free by Jos Miguel Vilaca Abstract Actualmente a certificac o da qualidade do software uma preocupac o crescente da comunidade empresarial e instituicional Esta necessidade induziu a comunidade cient fica a desenvolver enquadramentos te ricos para suportar tal certificac o Situando se apenas no paradigma de programac o funcional este projecto pretende ser a ponte entre dois estilos de programac o do referido paradigma o pointwise e o point free O pointwise o estilo mais usual e mais intuitivo mas menos adequado ao c lculo transforma o e verifica o de propriedades Em contraposi o tem se o point free que se apresenta como mais favor vel s opera es de c lculo transforma o e verifica o contudo perdendo na compara o com as mais valias do point free Mais concretamente este projecto apresenta as regras de convers o de c digo Haskell pointwise para c digo Haskell point free assim como as regras de cria o de padr es recursivos com base na defini o do tip
4. converter cada express o pointwise na aplica o de uma express o point free a uma vari vel ou a v rias vari veis Surge ent o um primeiro algoritmo em que se designa por PF a fun o de convers o de pointwise Para cada express o pointwise este algoritmo converte a num par ordenado cuja primeira componente uma express o point free e a segunda componente uma ou mais vari veis O significado deste par que a express o pointwise argumento equivalente aplica o da express o point free resultado s vari vel eis que s o a segunda componente deste par PF definida ent o como se segue 1 Para uma vari vel tem se que a aplica o da fun o identidade vari vel em causa PF x id x 2 Para uma constante tem se que a aplica o de uma fun o que devolve sempre o valor k a um argumento fantasma PF k const k 3 Para a aplica o de uma fun o b sica de aridade um f a uma sub express o exp e assumindo que se conhece a convers o da sub express o tem se a aplica o da composi o da fun o com a express o point free que adv m da convers o da sub express o s vari veis da j referida sub express o PF f exp let 9 0 PF ezp in f g 1 4 Para um par ordenado tem se a aplica o do produto das express es point free re sultantes das convers es das componentes ao par de vari veis cujas componentes adv m das sub convers es PF left r
5. fla f2ab uncurry f2 a b f3 abc uncurry uncurry 3 a b c f4 a b c d uncurry uncurry uncurry f4 a b c d a generaliza o parece ser fai an uncurry gt uncurry f a1 a2 an n 1 vezes para n N mas finito No caso de n ser um a composi o de zero uncurry s o elemento neutro da composi o a fun o identidade Contudo surgem problemas pois a express o do lado direito da igualdade n o represent vel nas express es point free actuais Um exemplo engra ado com uma fun o curried e de ordem superior e respectiva manipula o f a g b uncurry f a g b uncurry f idx g a b Mas como mecanizar o processo Tamb m aqui a ltima express o direita n o represent vel na nota o point free vigente Outro resultado que far possivelmente falta para suportar fun es curried uncurry f g f curry g Outra situa o vulgar em Haskell a jun o de casos cuja defini o igual n o fazendo pattern matching exaustivo por exemplo True ordering2Bool EQ ordering2Bool _ False Pretende se futuramente equipar a ferramenta com uma pr manipula o para ordering2Bool EQ True ordering2Bool LT False ordering2Bool GT False Afim de que ap s esta reescrita seja poss vel utilizar a ferramenta tal como est para obter a defini o point free equivalente ordering2Bool True False False
6. o deste padr o necess ria a introdu o dos conceitos de bifunctor e de tipos parametrizados Far se apenas esta introdu o por meio do exemplo das listas Pense se nas listas de elementos de um tipo A e nas listas de um tipo C Em Haskell definir se ia data List x Nil Cons x List x Suponha se uma fun o de A para C seja g A gt C Como definir a fun o f List A List C Usando o functor de listas tem se List A gt 1 A x List A OUtList A 9xf List C lt 1 C x List C Mist C Para completar o diagrama surgiu a fun o 1 gx f E a fun o g que faz realmente o mapeamento o resto apenas navega o e preserva o da estrutura Usando bifunctores o diagrama anterior convertido em List A gt B A List A Out List A f map f List C lt B C List C MList C A generaliza o que apenas se apresenta mas n o se justifica para um tipo indutivo parametrizado unariamente T tipos A e C e com uma fun o de convers o entre os ltimos tipos referidos g A gt C T A gt B 4 T A outr A f mapg B P TO lt B 0 TC inr c Como se pretendia uma breve exposi o sobre os padr es recursivos omitiu se a teoria de lgebras co lgebras functores e bifunctores entre outros assuntos Estes assuntos s o abordados de forma global e detalhada em Oli99b e Ven00 A Biblioteca Pointless e os Tipos Indutivos Relativamente ainda biblioteca Pointles
7. apenas a gera o da fun o out sendo a gera o da fun o in an loga Suponha se o tipo de dados indutivo anterior e nas mesma condi es IndT ype Para cada construtor Const cria se o respectivo injector inj no co produto de ari dade m Simbolicamente out Const argi1 agim inj by out Const ar gm Ar Jmm Mim bm com arg argumentos do tipo T j para i 1 Mm e j 1 ni Para cada i 1 m bi dado por 1 Se n zero o construtor Const n o tem argumentos ent o b a constante Note se que o nico elemento do tipo 1 que em Haskell representado por 2 se n maior do que zero ent o b ser um tuplo de n componentes este caso tamb m considera um tuplo de uma nica componente seja b cia Cim sendo que para cada y E 1 ni Gy a Se argi j uma vari vel simples ent o ci j arg b Se argi j um tuplo seja argij dias diga Ent o Cig le Cija sendo que para cada h 1 q a di jn aplica se a regra 2a ou a 2b para obter i j h Neste momento j poss vel gerar automaticamente toda uma inst ncia da classe FunctorOf para um tipo de dados indutivo 6 Convers o em Funcionamento O primeira problema que surge quando se come a a implementar a convers o de acordo com as ideias j apresentadas a parcialidade do processo a convers o s poss vel em alguns casos as limita es s
8. Haskell sobre o estilo de programa o point free e os seus combinadores sobre os tipos de dados indutivos e as suas propriedades e sobre os padr es de recursividade que est o associados aos tipos indutivos Mas principalmente este projecto abriu me as portas para um novo mundo o da investiga o cient fica facto que foi impulsionado pela minha inser o no PURe caf Refer ncias BdM97 Richard Bird and Oege de Moor Algebra of Programming Prentice Hall 1997 CP04 Alcino Cunha and Jorge Sousa Pinto Point free program transformation Technical Report DI PURe 04 02 03 Departamento de Inform tica Universidade do Minho February 2004 Avail able from http www di uminho pt pure Cun Gib02 MFP91 Oli99a Oli99b Ven00 Manuel Alcino Cunha Point free programming with hylomorphisms Unpublished note Jeremy Gibbons Calculating functional programs In R Backhouse R Crole and J Gib bons editors Algebraic and Coalgebraic Methods in the Mathematics of Program Construction volume 2297 of LNCS chapter 5 pages 148 203 Springer Verlag 2002 Erik Meijer Maarten Fokkinga and Ross Paterson Functional programming with bananas lenses envelopes and barbed wire In J Hughes editor Proceedings of the 5th ACM Conference on Functional Programming Languages and Computer Architecture FPCA 91 volume 523 of LNCS Springer Verlag 1991 Jos Nuno Oliveira An introduction to pointfree pro
9. Um tipo indutivo isomorfo aplica o do functor ao pr prio tipo e o menor tipo nestas condi es Simbolicamente para um tipo T e um functor F escreve se T uPeTSFT Se h um isomorfismo existem as duas fun es que o testemunham neste caso as fun es designam se in e out in a fun o que constr i um elemento do tipo indutivo e out a fun o que destr i um elemento do tipo no respectivo isomorfismo Simbolicamente T out TT TA FT e used in O functor F aplicado ao tipo T um co produto de tipos n rio um por cada modo de construir um elemento do tipo ou seja um por cada construtor Por exemplo para as listas declaradas em Haskell como data List Nil Cons Int List F List ser 1 Int x List Como visto anteriormente quando o dominio de uma fun o um co produto essa fun o um either Generalizando o resultado para o co produto n rio e o respectivo either n rio a fun o in um either cuja aridade o n mero de construtores Mais substituindo o tipo List por um seu isomorfo seja data List Nil Cons Int List a fun o o either dos construtores Para o segundo exemplo das listas vir in Nil Cons Assim a fun o in um either dos construtores do tipo salvo o rearranjo dos cons trutores para a vers o uncurried e a adi o do argumento aos construtores sem argu mento 2 4 Padr es Recursivos Os programadores que escreviam fun es
10. a defini o pointwise substitu da pela equivalente em point free Se se verificar algum erro na convers o dessa fun o os resultados parciais de convers o s o ignorados e a defini o pointwise mantida Relativamente s defini es de tipos de dados indutivos n o h convers o das mesmas mas apenas gera o de uma inst ncia tomando estas defini es como informa o Deste modo as defini es s o sempre mantidas e no caso de o processo de gera o da inst ncia FunctorOf para esse tipo ocorrer livre de qualquer erro acrescentada essa inst ncia Sucintamente sempre que ocorre um erro o c digo pointwise original mantido ou a inst ncia n o criada Na sec o 5 1 aquando da explica o do algoritmo PF surge o caso de aplica o de uma fun o b sica a uma express o Estas fun es b sicas t m aridade um tal como as express es point free que n o s o mais do que express es funcionais de aridade um escritas no estilo point free Assim poss vel generalizar a regra 3 de PF para PF f exp le 9 0 PF exp in f g 2 A defini o do algoritmo a mesma s que agora f pode ser al m de uma fun o b sica uma qualquer express o point free Tal como anteriormente exp uma express o Haskell g uma express o point free e x outra express o Haskell A implementa o actual abrange esta generaliza o A implementa o do algoritmo PF levantou um pequeno problema as express
11. facilmente apresentadas e implementadas neste estilo sendo as leis point free mais gen ricas Uma das cr ticas que apontada a este estilo de programa o a de que pouco intuitivo o significado dos programas point free dificultando portanto a sua escrita pelos programadores Este um dos motivos que mais tem contribu do para o pouco uso do estilo point free No entanto talvez n o seja o estilo que seja pouco intuitivo mas o facto de os programadores estarem habituados a pensar de forma diferente que o torne pouco utilizado Por todas estas caracter sticas vulgar fazer se a analogia entre o c lculo point free e as transformadas de Fourier que apesar de n o t o intuitivas se adequam melhor manipula o Antes de terminar esta sec o deixa se aqui um exemplo o da fun o que calcula a m dia dos elementos de uma lista de n meros reais A defini o pointwise m dia Float gt Float m dia 1 sum 1 length 1 e a defini o point free m dia Float gt Float m dia div sum length em que div a vers o uncurried de 2 2 Combinadores em Haskell Pointless Em Haskell o combinador composic o integra a biblioteca que importada por defeito e est portanto sempre acess vel Tamb m as fun es de projec o fst e snd se encontram nesta biblioteca standard Quanto aos outros podem ser usados em Haskell importando a biblioteca Pointless da autoria de Alcino Cunha e dispon
12. o de padr es apenas na primeira componente ou apenas na segunda Tomando as defini es ap s o passo de elimina o de vari veis vem 1 Exaust o de padr es apenas na primeira componente f ConstA xid pfez f ConstAm xid pfem com ConstA com 1 m todos os construtores de um tipo de dados indutivo e pfe express es point free para j 1 m A transforma o f pfeiX N pfem MdistL out x id 2 Exaustao de padroes apenas na segunda componente f idxconstB pfe f idx constB pfen com ConstB com i 1 n todos os construtores de um tipo de dados indutivo e pfe express es point free para j 1 n A transforma o neste caso f pre Ppfem NdistR id x out Outra dificuldade encontrada concerne tamb m a associatividade na implementa o os produtos e co produtos de tipos assim como os splits eithers produtos somas e composi es de express es point free n rios s o as vers es bin rias associadas direita Assim f pfeii pfein pfema pfemn NdistR NdistR m parcelas MdistL out X outB apresentado em 5 3 no ponto 3 passa e omitindo ainda os par ntesis da associativi dade da composi o para f pfe C Pferm 1 Pfern lt v V fena R ETE EE V a ea Val ejje NdistR NdistR NdistR m parcelas MdistL out X outB Surge ainda outra dificuldade MdistL
13. que envolviam tipos de dados indutivos cedo se aperceberam que muitas dessas fun es eram muito parecidas isto era poss vel encontrar padr es que se repetiam entre as diferentes fun es A partir do momento em que as linguagens passaram a suportar fun es de ordem superior ou seja fun es que recebem outras fun es como argumento capturaram se esses padr es em fun es Apresentar se o de seguida os padr es de recursividade de forma sucinta ao longo da exposi o relembre se que T uF Catamorfismo Este padr o depende essencialmente da estrutura do tipo indutivo que toma como argumento Assim pense se numa fun o f do tipo indutivo T para qualquer tipo X fixado previamente Sabe se j que poss vel passar do tipo T para F T pela fun o out e que o functor se aplica tamb m a fun es passando se assim de F T para F X por F f Suponha se uma fun o g F X gt X Diagramaticamente TFT dote Age A F f mant m a estrutura do functor no tipo substituindo os elementos do tipo T aqueles que criam a recursividade por elementos do tipo X que resultam de aplicar a fun o f aos elementos do tipo T A fun o g determina a fun o f pelo que g designada de gene gene do catamor fismo f Deste modo escreve se f lgl Anamorfismo Padr o dual do anterior em que o tipo indutivo que guia o padr o o do resultado da fun o isto este padr o serve para criar elementos de u
14. uma lista len Zero Succ len snd out facto bem conhecido que tal fun o b sica um catamorfismo de listas Manual mente faz se a manipula o que se segue len Zero Succ len snd out Zero Succ snd id x len out Zero id Suce snd idx len out Zero Succ snd id id x len out Zero Succ snd rec out cata Zero Suce snd com rec F len para F o functor de listas A possibilidade de automatizar este processo fica em aberto para trabalhos futuros 8 Conclus es Em v rias das refer ncias bibliogr ficas defendido que o estilo point free o mais adequado para raciocinar transformar ou provar propriedades de sobre programas Em todos estes trabalhos o intuito de mecanizar tais tarefas apresenta uma lacuna comum o c digo pointwise convertido em c digo point free em forma ad hoc sem que sejam apresentadas regras ou quais as justifica es dessa convers o Este trabalho vem suprimir essa lacuna e apresenta uma primeira teoria para a convers o de c digo pointwise em c digo point free diz se uma primeira teoria pois esta n o abrange toda a extens o do c digo pointwise nomeadamente fun es curried abstrac es fun es de ordem superior instru es de controlo como guardas e if then else embora uma sugest o seja j apresentada para estas instru es de refer ncia como let in e
15. vel online a partir de http wiki di uminho pt twiki bin view PURe PUReSoftware Aqui encontram se definidos os combinadores previamente apresentados com as seguintes representa es Split das fun es f e g representa se f NA g Either das fun es f e g representa se f g Produto das fun es f e g representa se f gt lt g Soma das fun es f e g representa se f g Fun o constante a representa se a Tamb m os injectores s o representados e s o no pelas fun es inl e inr respectiva mente para os injectores esquerda e direita Nesta mesma biblioteca e ainda no m dulo Pointless Combinators ainda poss vel encontrar a fun o app a gt b a gt b cujo resultado o de aplicar a primeira componente do argumento que uma fun o segunda componente e ainda o combi nador guarda que dado um predicado injecta o argumento num co produto sendo que a escolha do injector determinada pelo resultado do predicado sobre o argumento Este combinador representado pelo operador infixo e sua defini o pointwise p x if p x then inl x else inr x ou mais claramente p Az if p x then inl x else inr amp alternativamente a defini o pode ser dada como 5 _Jpz gt inlzx Pa Ta inr x Ainda nesta biblioteca mas agora no m dulo Pointless Isomorphisms est o definidas as fun es que testemunham os isomorfismos de tipos mais elementares Um isomorfismo de
16. Ab ina NY O argumento de vA a parte das vari veis do lado direito do ramo e e a vari vel ou tuplo de vari veis do lado esquerdo do mesmo ramo note se que ap s a aplica o do algoritmo PF foi poss vel separar a parte point free da parte com vari veis nos lados esquerdo e direito A fun o vA devolver a defini o da fun o variable Arrange e apesar de n o explicitamente expresso no algoritmo vA depende das vari veis do ramo tanto no lado esquerdo como no direito indicadas com e e el respectivamente note se que por abuso de linguagem se refere e na defini o acima sem que e surga nos argumentos 2 Na defini o acima surgiu esta nova fun o acede que gera a defini o da fun o variable Arrange fixada a vari vel x do lado direito e que depende da s vari vel eis no lado esquerdo O algoritmo implementado pela fun o acedeg Se se quer descobrir como aceder a uma vari vel x e o lado esquerdo uma vari vel uma das duas alternativas seguintes ocorrer e Ou a mesma vari vel x e a fun o que retorna a vari vel x do lado esquerdo a identidade e Ou as vari veis s o diferentes o que significaria que existia no lado direito uma vari vel n o existente no lado esquerdo Como visto anteriormente tal n o sucede Se se quer descobrir como aceder a uma vari vel x e o lado esquerdo um tuplo tendo em aten o que a vari vel x existe obrigatoriamente no lado esquerdo e s oco
17. al no ficheiro de c digo Haskell s o as declara es que surgem ap s a palavra where Veja se o exemplo length 0 length h t 1 length t Este bloco de c digo surge representado por um HsFunBind e cada uma das linhas de c digo representada por um HsMatch com e h t padr es HsPat e0 e 1 length t os lados direitos respectivamente para a primeira e a segunda linhas Neste exemplo n o h sub declara es Esta aproxima o an loga defini o de fun es por ramos na matem tica sendo que aqui o papel de ramos desempenhado pelos HsMatch s As defini es propriamente ditas tipo HsRhs suportam a representa o de guardas mas estas n o s o actualmente suportadas pela ferramenta Um exemplo muito simples de guardas max nm n gt m n n lt m m cujo significado o resultado de aplicar a fun o maz aos argumentos n e m n se se verificar a guarda n gt m e m se se verificar a guarda n lt m Em qualquer dos casos com ou sem guardas surgem as express es no caso de guardas ap s a condi o com o corpo da defini o Estas express es s o representadas pelo tipo HsExp cujos construtores mais relevantes s o HsVar vari veis HsCon construtores Por exemplo o EQ do tipo Ordering HsLit literais Por exemplo 1 a casa s o tr s literais HsInfixA pp operadores infixos por exemplo h t em que o operador infixo e h e t s o as sub express e
18. c digo de implementa o da representa o de express es point free 2 Point free e sua Motiva o A introdu o do estilo de programa o point free deve se a John Backus em 1977 na sua disserta o ACM Turing Award com o intuito de desenvolver um c lculo de programas que pudesse ser utilizado para a sua transforma o Desde logo o estilo point free se associou ao paradigma de programa o funcional n o s pelo seu enorme poder de programa o estrutural mas sobretudo por todo o poder alg brico e equacional que j ent o lhe estava subjacente Este estilo caracteriza se por programas que s o expressos como combina es de fun es mais simples Dois factos se destacam de imediato o primeiro que os argu mentos das fun es n o s o referidos desta inexist ncia de vari veis que adv m a designa o point free e o segundo que os combinadores funcionam como ligadores entre fun es mais simples ou express es constru das com os mesmos combinadores O objectivo inicial era o de criar um conjunto reduzido de combinadores que derivassem de formas categoriais standard estando desde logo estes combinadores equipados com um vasto conjunto de leis equacionais 2 1 Combinadores O primeiro combinador que surge pois j vulgarmente conhecido fora do contexto point free a composi o Pense se numa fun o f que aplicada ao resultado de aplicar uma outra fun o seja g a um argumento x Si
19. cia de FunctorOf criando para o programador a mesma facilidade que a escrita no c digo de deriving Eq para a gera o autom tica das fun es de igualdade Atente se ent o num tipo de dados indutivo gen rico IndT ype IndType p p Consti Tia Digg Consta Tm 1 Tm nm com l No m E N n1 Nm E No px par metros do tipo para k 1 1 Const construtores do tipo indutivo para 1 m e para i 1 m e j 1 ni T j tipos de dados que podem ser vari veis de tipo isto podem ser pj para algum j 1 1 ou construtores de tipo ou o tipo definido IndType p p ou ainda tuplos possivelmente encadeados das tr s alternativas anteriores Ficam assim exclu das as fun es de tipo e as aplica es de tipos O functor associado a IndT ype pi p ser um co produto de aridade m o n mero de construtores do tipo indutivo Simbolicamente escreve se X U Um Note se que por abuso de linguagem se utilizam os s mbolos e x que tamb m s o utilizados nas express es point free sem que no entanto sejam o mesmo estes s o operadores entre tipos e os anteriores s o operadores entre express es point free Para cada construtor Const com i 1 m os seus n argumentos de tipos respectivamente T 1 Tin d o origem a um produto com n componentes Uma excep o surge no entanto para os construtores de aridade zero n 0 caso em q
20. dida simplificadas quando executadas sobre os programas point free Sobre isto vejam se por exemplo os trabalhos An Introduction to Pointfree Programming Oli99a e Point free Program Transformation CP04 Com esta aproxima o point free ganha se gratuitamente conhecimentos matem ticos tais como uma vasta quantidade de leis alg bricas e equacionais e ainda m todos de c lculo j sobejamente estudados e cujo rigor est provado Isto sem d vida representa um atalho cujo rigor cientifico est garantido na teoria a desenvolver e um enorme ganho no c lculo e na transforma o de programas Mas e h sempre um mas sabe se que apenas um reduzido n mero de progra madores escreve os seus programas no estilo point free Assim sendo as t cnicas e tudo o resto que est associado ao c lculo e transforma o de programas atrav s do point free est o partida restritos a estes programadores Para ultrapassar esta restri o torna se pois necess rio converter os programas point wise nos seus equivalentes em point free podendo ent o ser aplicado o processo de c lculo e ou transforma o point free Fazer este processo manualmente acarreta um esfor o extra compar vel a escrever novamente os programas agora em point free e aumenta a probabilidade de introdu o de novos erros Surge assim a necessidade de desenvolver uma ferramenta capaz de automatica mente proceder convers o de pointwise em point free p
21. e NdistR n o s o fun es mas sim fam lias de fun es Repare se que os tipos s o MdistL T Zm 1 TIm xT T x T Tm 1 x T Tm x T NdistR T x Ty In 1 TIm Tx Ti HD x Tm 1 Tx Tm Assim para cada m gt 2e cada n gt 2 respectivamente MdistL e NdistR materializam uma fun o cuja defini o point free pode ser obtida por recorr ncia MdistL define se ent o como caso M 2 ent o MdistL distl caso M gt 2 ent o MdistL id M 1kistL distl em que distl a fun o definida em 2 2 e M 1 distL MdistLcom M a ser M 1 Analogamente define se NdistR como caso N 2 ent o NdistR distr caso N gt 2 ent o MistR id N l distR distr com distr e N 1 distR an logas a distl e M 1 distL respectivamente A implementa o de produtos e co produtos de tipos e de splits eithers produtos somas e composi es de express es point free n rios como as vers es bin rias associadas direita tamb m obrigam a uma reformula o da gera o da inst ncia FunctorOf Considerando ainda que na biblioteca Pointless a representa o das defini es dos functores usa os s mbolos para os co produtos e para os produtos a sec o 5 4 sofre as seguintes altera es X U U passa a X U Cae Um 1 Ung ces as regras para a defini o de U passam a 1 Se n zero ent o U Cons
22. ectivas defini es e o sexto argumento a lista de nomes de classes cujas inst ncias s o automaticamente geradas pelo interpretador compilador custa da defini o indutiva O segundo argumento representa o contexto dos par metros do tipo indutivo Este contexto que argumento de outros construtores ao longo de toda a representa o cont m informa o tal como o par metro a um qualquer tipo de dados que pertence classe Eq Este contexto pode conter m ltiplas ou nenhuma informa o semelhante do exemplo contudo tal desprezado na manipula o actual Saliente se que o objectivo da an lise da defini o de um tipo de dados indutivo a gera o de uma inst ncia de classe processo esse que ser descrito posteriormente confinando se a exposi o actual sem ntica da representa o de c digo Haskell na pr pria linguagem Quanto ao quinto argumento do tipo HsConDecl abrange construtores para records actualmente n o suportados e construtores de outros tipos de dados este ltimo tem como argumentos e por esta ordem o nome do construtor e a lista de tipos dos argu mentos do construtor definido esta ltima refer ncia a argumentos situa se a um n vel diferente Os tipos em Haskell podem ser ou dito de outro modo os construtores do tipo HsType s o a HsFun Hstype HsType HsTyTuple HsType tuplos tendo como argumento a lista dos tipos das compo nentes do tipo aten o pois o arg
23. era o do tipo de dados 3 3 Visualiza o Se se tem um tipo de dados necessita se de um modo de visualizar os elementos desse tipo Embora o Haskell forne a uma visualiza o standard esta n o a mais simples e intuitiva pelo que se optou por redefinir a fun o de visualiza o por forma a aumen tar a semelhan a com o que j foi exposto sobre os combinadores point free Uma das apostas de fundo foi visualizar os combinadores numa vers o infixa isto o s mbolo que representa o combinador surge entre os seus argumentos isto para os combinadores bin rios Assim foram tomadas as seguintes escolhas fun o b sica visualizada pelo respectivo nome composi o de sub express es o s mbolo que representa este combinador e split de sub express es o s mbolo que representa este combinador A produto de sub express es o s mbolo que representa este combinador gt lt either de sub express es o s mbolo que representa este combinador soma de sub express es o s mbolo que representa este combinador primeira projec o de um produto visualizada com a palavra fst segunda projec o de um produto visualizada com a palavra snd injector esquerdo de um co produto visualizado com a palavra inl injector direito de um co produto visualizado com a palavra inr constantes da linguagem o s mbolo que representa este combinad
24. es point free que dela resultavam eram muito longas e eram no desnecessariamente Assim optou se por aplicar uma fun o simplificadora de express es point free ao resultado do algoritmo PF As regras de simplifica o utilizadas s o g id g id g g fst snd id idxid id inl inr id id id id Estas regras s o aplicadas numa nica travessia e se se pensar na rvore da express o estas regras s o aplicadas pela ordem acima e de forma bottom up Relativamente a 5 3 a implementa o da jun o dos v rios ramos tamb m levantou problemas Como visto anteriormente o processo pode se aplicar repetidamente ao resultado da jun o anterior tal como sucede quando h composi es sucessivas de construtores Optou se ent o por implementar a jun o de ramos pelo m todo do ponto fixo vai se aplicando o processo de jun o sucessivamente ao passo de jun o anterior at que um passo de jun o produza o mesmo resultado que o passo anterior sendo retornado este resultado como o resultado do m todo Tendo se verificado que em alguns casos este m todo conduzia n o termina o modificou se a implementa o para o m todo do ponto fixo com limite de itera es isto significa que se ap s um n mero previamente fixado de itera es o m todo n o convergir para o tal ponto fixo o processo termina com o resultado desse momento Outra situa o que na implementa o careceu de aten o foi a a
25. gramming 1999 Draft document Jos Nuno Oliveira Recursion in the pointfree style 1999 Draft document Varmo Vene Categorical programming with inductive and coinductive types August 2000 A Manual do Utilizador Actualmente a ferramenta consiste num ficheiro execut vel A partir de um shell por exemplo bash poss vel utilizar a ferramenta de duas formas distintas 1 invocando a ferramenta passando como argumento na bash o nome do ficheiro Haskell com o c digo pointwise a converter Neste caso o resultado outro ficheiro de c digo Haskell total ou parcialmente point free colocado num ficheiro com o nome do ficheiro de entrada mas prefixado com GER Por exemplo supondo que o c digo Haskell pointwise est no ficheiro Example hs e fazendo a invoca o seguinte na bash pointfree Example hs surge um ficheiro GERExample hs com o resultado 2 invocando a ferramenta como filtro utilizando os redireccionamentos de bash Esta forma permite criar comandos de bash mais elaborados com execu o de outras opera es nomeadamente articula o com ferramentas geradoras de c digo ou de extrac o de c digo de ficheiros em literate Haskell Para o exemplo anterior far se ia a invoca o pointfree lt Example hs gt GERExample hs A invoca o da ferramenta em si n o levanta grandes quest es mas para que os resultados obtidos sejam o mais interessantes e completos poss vel necess rio tomar alguns cuidados co
26. ight let f x PF left g y PF right in fxg x y Reunindo se esta informa o obt m se o algoritmo seguinte PF x id x PER const k _ PF f exp let 0 2 PF ezp in f g 2 PF left right let f x PF left 9 y PF right in fxg x y com x uma vari vel k uma constante f uma fun o b sica de aridade um e exp left e right express es quaisquer Desde j se excluem fun es de aridade diferente de um e tuplos que n o sejam pares ordenados Contudo sempre poss vel codificar tuplos como pares ordenados encadeados isto a1 492 an com n Nen gt 2 pode ser convertido em ay a2 an 1 0n e a convers o pode ser efectuada em ambos os sentidos sem perda de informa o por outras palavras os tuplos gen ricos s o isomorfos aos pares encadeados direita Tamb m para as fun es de aridade superior a um poss vel contornar a limita o passando uma fun o b sica de aridade n N seja f ay ag an para uma fun o b sica f a1 a2 an que pelo j exposto passa a f a a2 an 1 0n Para as fun es b sicas de aridade zero a solu o que permite a aplica o do algo ritmo anterior torn las fun es de aridade um cujo argumento o Ultrapassar estas limita es significa que o utilizador tem de fazer manualmente as altera es sugeridas por forma a que o algoritmo PF conduza a resultados Talvez em vers es fu
27. lt Func string Comp pFExp1 pFExp2 Split pFExp1 pFExp2 Prod pFExp1 pFExp2 Either pFExp1 pFExp2 Sum pFExp1 pFExp2 Fst pl Snd p2 InL il InR 12 Const string Id i In fi Out fo ff string fc cata fs cata fp cata fe cata fm cata string pFExp1 pFExp1 pFExp1 pFExp1 pFExp1 fp fe fm pl p2 il i2 c i fi fo cata cata pFExp2 cata pFExp2 cata pFExp2 cata pFExp2 cata pFExp2
28. m o c digo pointwise Sempre que numa defini o de uma fun o surjam express es que envolvam e if then else e case of e let in e where e tuplos que n o s o pares ordenados os tuplos podem sempre ser convertidos em pares encadeados e guardas e ou ainda notac o mon dica a defini o pointwise do input imediatamente ignorada pelo processo de convers o Actualmente s a informa o presente no m dulo corrente pass vel de ser tratada pelo que defini es de fun es sobre tipos de dados indutivos definidos noutros m dulos mesmo que o Prelude n o s o convertidas para point free como seria expect vel Os construtores dos tipos de dados indutivos e as fun es ter o de ter aridade um para que seja poss vel a convers o nica excep o s o os operadores infixos com aridade dois que s o suportados Assim as fun es e os construtores curried ter o de ser alterados pelo programador para as respectivas vers es uncurried em que os argumentos est o em pares ordenados encadeados Por exemplo fabc a b c n o ser convertida mas g a b c atbte j convertida para point free O programador respons vel por garantir que a defini o exaustiva nos padr es e que estes s o disjuntos isto para uma fun o com um argumento de um tipo de dados indutivo t m de existir tantos ramos quantos os construtores do tipo indutivo um ramo por cada co
29. ma certa estrutura indutiva Sendo f o anamorfismo com f X gt Tego respectivo gene tem se o diagrama x FX f 0 r f T lt x FT in Hilomorfismo Basicamente este padr o a composi o de um catamorfismo com um anamorfismo Diagramaticamente Ts ON on r 9 lo T lt FT um r I Y r FY Este padr o tem assim dois genes o gene g do anamorfismo e o gene f do catamor fismo O tipo de dados indutivo que guia o hilomorfismo g f X Y o da estrutura interm dia T Paramorfismo Este padr o uma varia o do catamorfismo No catamorfismo ap s se efectuar a chamada recursiva n o mais poss vel recuperar a informa o da sub rvore qual feita a chamada recursiva Esta variante efectua a chamada recursiva e mant m a informa o da sub rvore duplicando a sub rvore e n o aplicando a chamada recursiva c pia Diagramaticamente T ou pr f lt lgl gt lt f id gt p F X xT Note se que neste padr o o tipo do gene mais elaborado g F X xT gt X Apomorfismo uma varia o do anamorfismo dual varia o do paramorfismo Aqui cria se um co produto antes das invoca es recursivas Diagramaticamente SPT f i gt f id T l FT n Note se que neste padr o o tipo do gene g X gt F X T Mapeamento Este padr o usado para converter toda a informa o numa estrutura mas mantendo intoc vel tal estrutura Para a explica
30. mbolicamente escreve se f g x Suponha se que se quer uma fun o h tal que f g x h x para todo o x no dom nio de y e tal que o contra dom nio de g esteja contido no dom nio de f Intuitivamente pensar se que h definida custa de f e g Define se ent o o combinador composi o e representa se pelo sinal que dadas duas fun es g A B e f B C devolve uma nova fun o h pretendida f g A gt C cuja defini o pointwise f gx fglz Diagramaticamente dt eee See fg Usam se aqui as defini es pointwise para ambientar o leitor desconhecedor do estilo point free com os combinadores usando algo que lhe previamente conhecido Al m disso existe um conjunto minimo de combinadores que tem de ser expresso em pointwise Suponha se agora o caso de duas fun es que partilham o mesmo dominio isto fun es f e g tais que f A gt Beg ASC Como as combinar Uma possibilidade uma fun o h A gt BxC O combinador que permite expressar a fun o h custa das fun es f e g denomi nado split Existem duas representa es usuais para o split das fun es f e y f g lt f g gt A defini o pointwise lt f g gt x f 2 92 O respectivo diagrama de tipos c c lt 7 px tea A B em que 7 e ma s o respectivamente a primeira e a segunda projec es tamb m representadas pelas fun es fst e snd respectivamente e em Haskell As defini es pointwi
31. mes deixa facilmente adivinhar essa correspond ncia Assim sempre poss vel converter um padr o HsPat numa express o HsExp Neste momento j se sabe representar tanto o c digo Haskell como as express es point free mas como fazer a convers o Ser sempre poss vel faz la Se n o em que situa es Este o tema que se abordar de seguida 5 Teoria de Convers o Tal como para qualquer outro problema o processo de convers o pode ser partido em sub problemas aplicando assim o lema divide to conquer Apresentam se de seguida as v rias fases em que se partiu a convers o 5 1 1 Passo A defini o de uma fun o consiste tipicamente num conjunto de ramos no sentido matem tico de fun es definidas por ramos Cada ramo cont m um lado esquerdo e um lado direito relativamente ao sinal de e em ambos os lados podem ocorrer vari veis vari veis essas que se pretende remover Foque se a aten o num dos lados neste momento irrelevante se o esquerdo ou o direito pois sob certa perspectiva eles s o iguais Podem se encontrar express es como g X h 2 3 j Just 1 com f g he j fun es de um argumento x uma vari vel e Just um construtor de aridade um Por exemplo g x significa a aplica o da fun o g vari vel x Mas g por si s j uma express o point free Pode se ent o converter g x na aplica o da express o point free g vari vel x Analogamente tentar se
32. nda reescrever usando a defini o de composi o de fun es como fe g variableArrange e Usando a defini o matem tica de igualdade de fun es e sendo e uma vari vel qualquer e portanto pass vel de ser quantificada universalmente vem f g variableArrange Z E pois agora necess rio efectivar a suposi o definindo a fun o variable Arrange que garante a igualdade e variableArrange e O que se far de seguida apresentar as fun es que geram a defini o da fun o variable Arrange que necess ria em cada ramo de uma fun o sendo que esta gera o depende de ambos e e e 5 2 Rearranjo das Vari veis O processo de gera o da fun o variable Arrange desenrola se em duas partes 1 Tal como e e pode ser uma vari vel simples ou um par em que uma ou as duas componentes podem ser novos pares ou vari veis Assim Para o caso em que e uma vari vel simples basta saber como aceder a essa vari vel em e Chame se a esta fun o que acede vari vel x acede e que apenas depende da estrutura e posi o da vari vel x no lado esquerdo Para o caso em que e um tuplo ej eh descubra se as fun es variable Arrange de cada uma das coordenadas para e Sejam estas fun es vA e vAg Tem se que e vA e e vAz e de onde e4 e5 vA e vA e e que o mesmo que e e1 e vA A vAz e Algoritmicamente tem se vA x acede e vA a b leta vAa b v
33. nstrutor com os construtores explicitamente presentes nos padr es Por exemplo data Nat Zero Succ Nat f Zero a 1 n o convertido tal como n o o se se acrescentar no fim do c digo anterior a linha f _ 2 Mas data Nat Zero Succ Nat f Zero a f Succ n l Ne j convertido Tamb m o caso data Tipo Const1 Const2 Const3 f Tipo gt Int f Const1 _ 1 f 2 n o convertido mas se o programador alterar para data Tipo Const1 Const2 Const3 f Tipo gt Int f Consti _ 1 f Const2 _ 2 f Const3 _ 2 j convertido para point free Contudo algumas flexibilidades foram j introduzidas E poss vel alterar a ordem dos ramos numa defini o sem que isso altere a convers o Por exemplo fib Zero a Succ Zero a fib Succ Zero a Succ Zero a fib Succ Succ a plus fib Succ a fib a e fib Succ Succ a plus fib Succ a fib a fib Zero a Succ Zero a fib Succ Zero a Succ Zero a resultam na mesma defini o em point free No caso de ordem dos r pares de construtores no argumento de uma fun o poss vel trocar a amos e n o efectuar exaust o de padr es numa das componentes Por exemplo plus Zero plus Succ abrevia plus Zero plus Zero plus Succ plus Succ a C c n c Succ plus n c a Zero b Zero b a Succ b Succ b n Zero b S
34. o de dados indutivo Por forma a efectivar estas ideias s o tamb m apresentadas bibliotecas e uma ferramenta que automatizam tais tarefas 1 Introdu o Desde h longos anos que a comunidade cient fica procura modos de lidar tratar e pensar os programas inform ticos Esta procura converge com as pretens es das empresas e institui es de terem garantias da qualidade desses programas e de os poderem melhorar tornando os mais eficientes em tempo e ou espa o sem perda das garantias de qualidade j adquiridas Um paradigma em que tal esforco tem sido efectivo o funcional Este paradigma defende o princ pio de programas estruturados como a chave para software de qualidade e capaz de garantir essa mesma qualidade isto n o se quer software cuja qualidade surge do acaso mas software de qualidade certificada Actualmente pensa se que o c lculo e a transformac o de programas funcionais poder o ser mais simples sobre programas point free Antes de mais conv m salientar o que se entende por programas point free numa defini o muito elementar s o progra mas que n o cont m vari veis em oposi o obviamente com os programas com vari veis ditos pointwise Mas afinal o que significa o c lculo e a transforma o de programas s o mais simples sobre programas point free Raciocinar calcular e manipular quer seja para transfor mar o programa ou para provar propriedades sobre o mesmo s o ac es em grande me
35. o referidas ao longo deste relat rio E o que fazer quando um desses passos de convers o falha Tendo em aten o que a linguagem de implementa o o Haskell as Monads s o a resposta bvia para resolver esta situa o Assim uma fun o que implementa um passo de convers o e tem tipo A gt B mas que pode falhar passa a ter tipo A gt MyMonad B em que MyMonad uma Monad a definir Esta aproxima o mon dica permite a cria o expl cita de erros e trata automaticamente da propaga o dos mesmos Inicialmente o objectivo da utiliza o de uma Monad era o de implementar ape nas a parcialidade do processo adequando se para este fim a Monad Maybe Contudo com o evoluir da implementa o surgiu a necessidade de incluir tamb m informa o global Com apenas algumas modifica es principalmente a redefini o de MyMonad passou se da Monad Maybe para a Monad StateT St Maybe com St um tipo de dados para acomodar a informa o global a Monad StateT a m est definida na biblioteca Control Monad State Os erros v o sendo propagados atrav s da Monad mas a um n vel superior eles t m de ser tratados Onde Um ficheiro de c digo cont m v rias defini es de fun es e de tipos de dados in dutivos convers o de uma fun o n o depende de outra pelo que o mbito dos erros deve ser restrito defini o onde este ocorre Assim quando a convers o de uma defini o de uma fun o ocorre integralmente sem erros
36. or e precedido da palavra que representa a constante a fun o especial identidade visualizado com a palavra id a fun o in visualizado com a palavra inn a fun o out visualizado com a palavra out O leitor mais atento detectou a proximidade desta visualiza o com a utiliza o da biblioteca Pointless Tal foi intencional para permitir o uso dessa biblioteca A vers o actual de visualiza o muito verbosa no sentido em que coloca demasia dos par ntesis Relembre se que a defini o de diferentes preced ncias para os operadores permite a omiss o de muitos dos par ntesis De acordo com as metodologias de programa o referidas foi tamb m definido o cata morfismo para este tipo de dados Contudo surge aqui uma diferen a relativamente ao exposto genericamente enquanto genericamente se considera um nico gene que tipi camente um either de fun es mais simples nesta implementa o tem se um tuplo de genes um por cada construtor do tipo de dados PFExp Para mais detalhes sobre a tipo de dados PFExp assim como a sua visualiza o e o catamorfismo associado consultar o anexo B onde se encontra a implementa o em Haskell 4 Representa o Interna do C digo Haskell Sendo pretens o desta ferramenta a convers o de c digo Haskell pointwise em c digo point free s o necess rios meios para manipular esse c digo que se encontra em ficheiros Duas abordagens s o poss veis a p
37. or forma a que o facto de os programas serem escritos no estilo pointwise n o penalize o seu tratamento com as t cnicas point free O objectivo deste projecto ent o a cria o desta ferramenta de convers o para os programas Haskell esta ferramenta ser aqui designada de pointfrezador Institucionalmente este projecto enquadra se no projecto de investiga o Program Understanding and Re engineering Calculi and Applications POSI ICHS 44304 2002 abreviado para PURE financiado pela Funda o para Ci ncia e Tecnologia e que decorre no Departamento de Inform tica da Universidade do Minho O projecto alvo deste relat rio contextualizado no PURe e especialmente nos trabalhos de Alcino Cunha e Jorge Sousa Pinto Destacam se desde j os trabalhos Point free Program Transformation CP04 in vestiga o conjunta dos autores referidos anteriormente e Point free Programming with Hylomorphisms Cun da autoria de Alcino Cunha E ent o com nimo que se inicia o projecto ciente contudo da impossibilidade de criar a ferramenta total e perfeita Estrutura do Relat rio No cap tulo 2 far se uma introdu o ao point free o que quais as suas van tagens e limita es Nas sec es far se a apresenta o e defini o dos combinadores 2 1 uma introdu o de uma sua implementa o em Haskell a biblioteca Pointless 2 2 uma apresenta o sucinta dos tipos indutivos e das suas propriedades 2 3 e uma cu
38. ora manipular estas express es at que as v rias igualdades se fundam numa s em que o lado esquerdo unicamente o nome da fun o b sica Nesta altura a fun o b sica cuja defini o pointwise foi dada ser definida equivalentemente pela express o point free calculada Suponha se que se tem um tipo indutivo IndType Const Type Const Typen em que n N Const s o construtores de aridade um para 1 n e Type para 1 n s o tipos de dados Em Haskell viria data IndType Const_1 Type_1 Const_n Type_n 1 Suponha se ainda que se tem uma func o b sica f total e cujo argumento do tipo indutivo definido acima ou seja f IndType gt TypeA com TypeA um tipo de dados arbitrariamente fixado Sendo f uma func o total no caso geral ter um ramo por cada construtor do tipo indutivo argumento Suponha se a seguinte defini o pointwise para f f Consty x1 rhs f Consta x2 rhs f Consta n Ths com T1 92 Xn Vari veis ou tuplos possivelmente encadeados de vari veis e rhsiy rhsa rhsn express es Aplicando as transforma es propostas at agora surgiria f Consti rhsP vA f Const rhsPa vAz f Constn rhsPn vAn tais que rhs rhsP vA xi e rhsP e vA s o express es point free para todo o1 1 n Tendo em conta a igualdade estrutural do either n rio obt m se f Const f Constz f Constn rh
39. out Tamb m para express es if then else se pondera uma solu o dada a express o if cond x then fl x else f2 x Com cond uma fun o de um argumento que retorna um booleano x uma vari vel ou tuplos possivelmente encadeados de vari veis e fl e f2 fun es de um argumento com o mesmo tipo para o resultado convers o ser possivelmente f1 f2 cond x Quanto a padr es suponha se o seguinte caso f x pred1x rhs_1 x predn x rhs_n x otherwise rhsdefault x com n N x uma vari vel ou tuplos possivelmente encadeados de vari veis pred para i 1 n uma fun o booleana de aridade um e para cada i 1 n rhs uma fun o de aridade um sendo que todos os rhs t m o mesmo tipo para o resultado e que ainda o mesmo de rhsdefault Pensando os padr es como if s encadeados vem f x if pred_1 x then rhs_1 x else if pred_n x then rhs_n x else rhsdefault x Utilizando a regra de convers o proposta para os if then else vem f rhsi rhsn rhsdefault pred predi As limita es para as regras de convers o tanto para os if then else como para os padr es s o acentuadas as vari veis t m de ser sempre a mesma e as fun es de aridade um referidas t m de ser j express es point free Atente se agora na defini o point free que se obt m actualmente para a fun o b sica que calcula o comprimento de
40. ra o output Em Haskell existem diferentes declara es o que testemunhado pelos v rios con strutores do tipo HsDecl cujos nomes permitem regra geral identificar a sem ntica que lhes est associada Assim pode se ter declara es de tipos de dados declara es de tipos de dados indu tivos declara es de operadores infixos declara es de classes declara es de inst ncias de classes declara es de tipo de express es tamb m conhecidas por assinatura de tipo da express o e declara es de fun es entre outros Apenas se revestem de import ncia os construtores HsDataDecl HsInstDecl e HsFunBind respectivamente para as declara es de tipos de dados indutivos inst ncias de classes e fun es Daqui em diante os argumentos do tipo SrcLoc ser o ignorados na exposi o tal como o foram no tratamento na ferramenta pois representam informa o de posiciona mento no ficheiro de c digo fonte que de todo desnecess ria 4 1 Tipo de Dados Indutivo Comece se pela declara o de tipos de dados indutivos cujo construtor HsDataDecl e tem a seguinte assinatura HsDataDecl SrcLoc gt HsContext gt HsName gt HsName gt HsConDec1 gt HsQName gt HsDecl O terceiro argumento representa o nome atribu do ao tipo de dados indutivo o quarto a lista com os nomes dos par metros do tipo indutivo o quinto e principal a lista de construtores declarados para o tipo conjuntamente com as resp
41. rec 1 e2 parF n where parA 0 showString parA 1 showChar parF O showString parF 1 showChar instance Show PFExp where showsPrec _ Func str showString str showsPrec n Comp el e2 showsPrec 1 el showString showsPrec 1 e2 showsPrec n Split el e2 auxP n el e2 showsPrec n Prod el e2 auxP n el e2 gt lt showsPrec n Either el e2 auxP n el e2 AN showsPrec n Sum el e2 auxP n el e2 showsPrec _ Fst showString fst showsPrec _ Snd showString snd showsPrec _ InL showString inl showsPrec _ InR showString inr showsPrec _ Const str showString const showString str showsPrec _ Id showString id showsPrec _ In showString inn showsPrec Out showString out the cataphorphism function for the PFExp datatype cataPFExp String gt a for functions a gt a gt a for composition a gt a gt a for split a gt a gt a for product a D a gt D a for either a gt a gt a for sum gt gt M m p y String a a a gt PFExp gt a cataPFExp ff fc fs where cata cata cata cata cata cata cata cata cata cata cata cata cata cata for fst for snd for il for i2 gt a for constant function gt for id function for in function gt for out function a the input pointfree expression a the final resu
42. rimeira consiste em manipula o directa de strings a segunda consiste em usar um parser que gere uma rvore abstracta Dada a quantidade de manipula es necess rias a primeira abordagem torna se de sajustada Usar se ent o a segunda com o parser disponibilizado na biblioteca Lan guage Haskell Parser que actualmente uma biblioteca distribu da com os compiladores e interpretadores de maior utiliza o Este parser retorna um elemento do tipo HsModule que na actualidade a representa o standard de c digo Haskell e providenciado pela biblioteca Language Haskell Syntax na realidade este elemento retornado mas en capsulado numa Monad contudo tal n o neste momento relevante para a exposi o Procurar se dar uma breve explica o da forma como o c digo Haskell represen tado neste tipo de dados No entanto dada a vastid o deste tipo de dados confinar se a exposi o aos que s o relevantes no contexto deste projecto Um ficheiro de c digo Haskell considerado um m dulo HsModule Este HsModule cont m informa o sobre o nome do m dulo a localiza o no ficheiro fonte a lista de exporta es aquilo que se permite que seja visto e utilizado do exterior do m dulo a lista de m dulos importados e aquilo que realmente relevante que a lista de declara es defini es do m dulo apenas esta lista ser alvo de manipula o neste pro jecto sendo os restantes argumentos propagados pa
43. ro a fib Succ Succ a plus fib Succ a fib a fib Nat gt Nat fib Succ Zero Succ Zero plus fib Succ gt lt fib id A id out out nat2Int Nat gt Int nat2Int Zero _ 0 nat2Int Succ n 1 nat2Int n nat2Int Nat gt Int nat2Int 0 CCuncurry CC 1 gt lt nat2Int id A id out zipi List a List b gt List a b zipi Nil a Nil _ Nila zip1 Nil a Cons _ Nila zip1 Cons _ Nil b Nil b zip1 Cons x xs Cons y ys Cons x y zip1 xs ys zipl List a List b gt List a b zipl Nil fst Nil Est Nil snd Cons id gt lt zip1 fst fst A fst snd A snd fst A snd snd distr distr distl out gt lt out 7 Ideias em Evolu o Como referido por diversas vezes a ferramenta no estado actual n o trata algumas situa es Para algumas dessas situa es foram surgindo ideias que apesar de n o terem sido incorporadas na ferramenta se pretende registar aqui Algumas ideias n o foram integradas por dificuldades de tempo e de implementa o enquanto que outras carecem ainda de generaliza o e ou fundamenta o te rica ade quada pelo que dever o ser tidas como pontos de partida para solu es e n o como solu es propriamente ditas No que concerne as fun es curried poss vel afirmar as seguintes igualdades fia
44. rre uma nica vez em Haskell uma vari vel s pode ocorrer uma vez no lado esquerdo de um ramo de uma fun o isto conhecido por padr es lineares conclui se que e sea vari vel x aparece algures na primeira componente do tuplo a fun o que lhe aceder ser a composi o da fun o que acede a x na primeira componente com a projec o da primeira componente e Quando a vari vel x ocorre na segunda componente o resultado an logo s que agora usa se a segunda projec o Isto pode representar se como acede Xx id aceder a b x ocorre em a acede a fst z ocorre em b acede b snd Note se que id n o significa que acede x uma fun o que aguarda outro argumento e o devolve mas sim que a defini o da fun o variable Arrange que se pretende gerar neste caso a fun o identidade O contexto em que esta fun o acede utilizada garante que os casos que foram propositadamente omitidos n o ocorrem Conclui se ent o que o rearranjo das vari veis depende numa primeira fase da es trutura e posicionamento das mesmas no lado direito e que sempre que se encontra uma vari vel simples no lado direito a segunda fase apenas depende da estrutura e posicionamento da vari vel em causa no lado esquerdo Garantida que est a suposi o tem se no estado actual e para cada fun o um conjunto de igualdades entre express es point free 5 3 Jun o dos V rios Ramos O objectivo ag
45. rta explana o dos padr es recursivos que est o associados aos tipos indutivos 2 4 nomeadamente uma refer ncia implementa o deste padr es na biblioteca Pointless 2 4 No cap tulo 3 aborda se como se representam as express es point free neste trabalho apresentando o tipo de dados que suporta a representa o 3 1 as limita es da repre senta o escolhida 3 2 e ainda o modo como se visualizam as express es point free 324 O capitulo 4 concerne a representa o do c digo Haskell neste trabalho afim de poder ser manipulado As sec es desta referem se representa o das constru es da linguagem Haskell que s o relevantes no mbito deste trabalho O cap tulo 5 aborda a teoria subjacente convers o de point free para pointwise o prop sito deste trabalho As tr s primeiras sec es explicam as diferentes fases da convers o enquanto a ltima 5 4 explica a gera o autom tica das fun es in e out de tipos de dados indutivos O cap tulo 6 explica a um n vel bastante abstracto como implementar as ideias do cap tulo anterior e tem uma sec o com alguns exemplos de utiliza o No cap tulo 7 referem se algumas ideias que n o foram implementadas e situa es para as quais n o se conhece a convers o embora algumas indica es se tenham encon trado O cap tulo 8 apresenta as conclus es e o trabalho futuro Em ap ndice surgem um manual de utiliza o da ferramenta de convers o e o
46. s de entre os muitos aspectos de interesse destaca se ainda a classe Functor0f que permite que o programador associe a um tipo de dados indutivo o seu functor e as fun es de in e out Criada a inst ncia a biblioteca equipa o tipo indutivo com o functor as fun es in e out e ainda os padr es de recursividade mapeamento catamorfismo anamorfismo hilomorfismo paramorfismo apomorfismo e zygomorfismo 3 Representa o de Express es Point free 3 1 Tipo de Dados Para se poder criar e manipular express es point free necess rio primeiro definir uma forma de as representar Como visto anteriormente as express es point free podem ser fun o b sica interessa apenas o seu nome composi o de sub express es split de sub express es relembra se que o split aplica duas fun es a um mesmo argumento devolvendo o par de resultados produto de sub express es duas fun es s o aplicadas sendo que cada uma das fun es aplicada respectiva componente do par dado como argumento either de sub express es aplicada uma ou outra das fun es consoante o injector do argumento soma de sub express es id ntica anterior s que enquanto a anterior destr i o injector esta ap s aplicar uma das fun es restitui o injector inicial projec es de um produto para um par existem duas projec es que se designam vulgarmente primeira e segunda injectores de um co produto
47. s podem acontecer Os e se a vari vel argumento arg do tipo IndType p pj ent o cij Id argi e se a vari vel argumento arg j n o do tipo IndT ype p p ent o cij Const argi j Os b Se arg j um tuplo seja arg dij1 digg ent o cij espa is xi essg 2 eia sendo que para cada h 1 q a di jn aplica se a regra 2a ou a 2b para obter e jn 6 1 Exemplos Termina se este cap tulo apresentando alguns exemplos de convers o Estes exemplos s o obtidos automaticamente pelo uso da ferramenta de convers o que implementa as ideias at agora explanadas Eis ent o os exemplos data Nat Zero Succ Nat deriving Show Eq instance Functor0f Const Id Nat where inn Inl Const Zero inn Inr Id v1 Succ vi out Zero Inl Const out Succ vi Inr Id vi data List a Nil Cons a List a deriving Show Eq instance Functor0f Const Const a Id List a where inn Inl Const Nil inn Inr Const vi Id v2 Cons v1 v2 out Nil Inl Const out Cons vi v2 Inr Const vi Id v2 fact Nat gt Nat fact Zero a Succ Zero a fact Succ n mult Succ n fact n fact Nat gt Nat fact Succ Zero mult Succ gt lt fact id A id out fib Nat gt Nat fib Zero a Succ Zero a fib Succ Zero a Succ Ze
48. s respectivamente esquerda e direita HsApp aplica o de uma fun o a uma express o HsNeg App sinal de un rio HsLambda express es HsLet nota o let in Hslf nota o if then else HsCase nota o case of HsDo nota o do HsTuple tuplos com um n mero arbitr rio de componentes HsList listas por extens o HsParen par ntesis HsLeftSection vers o curried para os operadores infixos em que o argumento direita est em falta HsRightSection vers o curried para os operadores infixos em que o argumento esquerda est em falta HsEnumFrom enumera es por exemplo 1 HsEnumFromTo enumera es por exemplo 1 10 HsEnumFromThen enumera es por exemplo 1 3 HsEnumFromThenTo enumera es por exemplo 1 3 10 HsListComp listas por compreens o HsExpTypeSig express es com o tipo expl cito HsAsPat suporte para dupla referencia em que a segunda pode conter padr es Por exemplo 1 h t HsWildCard o s mbolo _ em Haskell A ferramenta tal como se encontra actualmente n o suporta grande parte destes construtores mas desde j objectivo a m dio prazo alargar o leque de express es suportadas Para os padr es tem se um conjunto mais reduzido de construtores mas cada cons trutor para padr es tem um correspondente em HsExp A proximidade dos no
49. sP vA rhsP2 vAz2 rhsPn vAn Aplicando agora a generaliza o n ria da fus o em sentido inverso vem f Const Consta N N Consta rhsP v y rhsP2 vA2 rhsPy vAn Tomando a defini o da fun o in de um tipo de dados indutivo que o either dos construtores surge fin rhsP vA1 rhsP2 vAg rhsPn vAn Compondo ambos os lados com a fun o out aparece f in out rhsPi vAi rhsP2 vA2 rhsPy vAn out Como in e out s o fun es mutuamente inversas e a identidade o elemento neutro da composi o vem f rhsP vAs VrhsPa v Ag rhsPy vAn out J se sabe ent o como transformar algumas defini es pointwise na equivalente defini o point free mas s no caso bastante particular de aplica o da fun o b sica a cada um dos construtores do tipo indutivo que argumento Pense se agora em se relaxar as condi es anteriores por exemplo pondere se o caso que ap s o passo de elimina o de vari veis d f Const Consti1 pfeia f Const Consti2 pfe12 f Const Constin pfeiny Consta Consta Pfem Constm CONStm 2 P Fem 2 f Constm CoNo Pim com Consty Constm todos os construtores de um tipo de dados indutivo e para cada i 1 m Consti a Consti n s o todos os construtores de um tipo indutivo Se se aplicar a lei anterior m vezes mas instanciando f com f Consty para k
50. se das projec es s o fst a b a snd a b b Dualmente pense se em duas fun es que partilham o mesmo co dominio sejam f B gt Aeg CHA O dual do produto de tipos o co produto de tipos pelo que se sup e h B C A O combinador que constr i a fun o h a partir das fun es f e g o either sendo que tamb m este tem duas representa es usuais f g Fe Denominando os injectores do co produto por inl e inr com inl B gt B4C e inr C B C tem se a seguinte defini o pointwise f g Cel a efa 9 inr x e Diagramaticamente evidenciada a dualidade B inl B et C A Surge ainda o combinador produto que se representa com o operador x e que dadas duas fun es f A Ceg B gt Dd a fun o fxg AxB gt CxD sendo que esta ltima func o pode ser definida recorrendo ao combinador split como fxg lt fim 9 72 gt O diagrama de tipos para este combinador AR ASB B id xe E m mo C C x D D e a respectiva defini o pointwise f xg a b f a g b Dualmente no co produto tem se o combinador soma que se representa pelo ope rador e que combina duas fun es f A gt C eg B gt D dando uma fun o f g A B C D e cuja defini o point free F g inl f inr g e em pointwise Diagramaticamente vem inl inr A A B Os combinadores j apresentados eram todos bin rios Surge agora um combinador
51. ssociatividade da composi o Na explana o escreve se f g h com f g e h fun es para representar tanto f g h como f g h Contudo na pr tica a implementa o distingue as e surgem situa es em que necess rio passar uma express o com associatividade esquerda como f g h para a equivalente com associatividade direita f g h Em 5 3 no ponto 2 refere se que no caso de m ltiplas composi es de construtores a sua elimina o ocorre da direita para a esquerda tornando se necess rio associar todas as composi es esquerda para a aplica o das regras descritas Tamb m relativamente jun o de ramos no caso de produtos de construtores sur giram dificuldades mas tamb m simplifica es A simplifica o concerne as fun es em que para todos os padr es de uma das compo nentes o resultado o mesmo isto fun es em que s se pretende exaust o de padr es numa das componentes E o caso de plus Nat Nat gt Nat plus Zero a Zero b Zero b plus Zero a Succ b Succ b plus Succ n Zero b Succ plus n Zero b plus Succ n Succ b Succ plus n Succ b que pode e deve ser abreviado para plus Nat Nat gt Nat plus Zero a c c plus Succ n c Succ plus n c e cuja defini o point free plus Nat Nat gt Nat plus snd Succ plus distl out gt lt id Pensando na generaliza o surgem dois casos exaust
52. t 2 Se n maior do que zero ent o U V 1 x uu x AE Via as Em que cada V deriva de T para todo i 1 mje j 1 n de acordo com as regras que se seguem a Se T IndType py p ent o V n o sen o Id representa a recursividade do tipo b Se T j pk para algum k 1 1 ent o Vij Const pk c Se T j um construtor de tipos de aridade zero por exemplo Int ent o V j Const Ti j d Se T j um produto de tipos de aridade q ent o V um produto de q factores em que a cada um deles s o aplicadas as regras 2a a 2d isto Vig Wija e e ve Wijgi 2 Wija em que tomando T como Y j1 X X Y jq cada Wij deriva de Y jn para todo o h 1 q usando as regras de deriva o 2a a 2d Obviamente a altera o dos tipos de dados implica altera es nas fun es in e out Assim inj define se como e para i 1 inji Inl e para i 2 n 1 inji Inr Inr Inl i 1 parcelas e para i n inji Inr cc Inr n 1 parcelas As regras de gera o de b passam a 1 Se n zero o construtor Const n o tem argumentos ent o b Const 2 se n maior do que zero ent o b ser um tuplo de n componentes este caso tamb m considera um tuplo de uma nica componente seja Ca e loss ja EE Cias El sendo que para cada j 1 ni cig a Se argi j uma vari vel simples ent o duas situa e
53. ta es Esta representa o contudo limitada na sua expressividade O facto de representarmos uma fun o b sica apenas pelo seu nome restringe a representa o a fun es cuja aridade n mero de argumentos um Deste modo perde se a capacidade de expressar fun es curried ou seja fun es de N argumentos que s o vistas como fun es de um argumento que retornam uma nova fun o de N 1 argumentos Tamb m as fun es de ordem superior ficam exclu das com esta representa o dado que n o h informa o sobre a s func o 0es argumento s Atente se ainda que com esta representa o os construtores s o meras fun es obri gatoriamente de aridade um Para este caso em que a linguagem alvo de transforma o o Haskell era poss vel eliminar os construtores Fst Snd InL InR Id In Out utilizando a seguinte tradu o Fst Func fst Snd Func snd InL Func Left InR Func Right Id Func id In Func inn Out Func out Para estas duas ltimas tradu es tamb m necess rio tomar em considera o a utiliza o da biblioteca Pointless e algumas das defini es nela contidas A op o por manter estes construtores ao n vel da nossa representa o deve se s facilidades que da adv m para a manipula o das express es point free Al m disso torna poss vel a altera o da linguagem alvo sem que isso implique a alt
54. tipos um par de fun es entre os tipos tais que as fun es s o mutuamente inversas isto sejam os tipos X e Y e as fun es f X gt Y e g Y X verifica se que f g id g f id Diz se ent o que X isomorfo a Y e escreve se X Y Na perspectiva da programa o dizer que os tipos s o isomorfos significa que poss vel converter os dados representados num tipo para a representa o no outro tipo de dados sem que haja perda de informa o Os isomorfismos definidos ent o no m dulo s o swap TO TTT EY AxB BxA swap coswap AT A B xC AxC BxC undistl distr AAA O E Cx A B CxA CxA ou ss op undistr assocl TT S Ax BxC Ax B xC Se pu assocr coassocl BSE A B C A B C coassocr 2 3 Tipos Indutivos At agora falou se de tipos de dados gen ricos Contudo existem certos tipos de dados com propriedades particulares que interessa aqui referir os tipos de dados indutivos Estes tipos de dados podem ser definidos recorrendo a eles pr prio designando se tal fen meno por recursividade Algo que conhecido destes tipos de dados que t m a eles associados um functor de tipo Sem se querer entrar em muito detalhe o tipo indutivo o menor ponto fixo menor solu o para uma equa o envolvendo um functor Mais exactamente o functor uma aplica o quer de tipos para tipos quer de fun es para fun es que captura a estrutura da defini o do tipo
55. tradicionalmente os dois injectores designam se es querdo e direito fun o constante permite representar as constantes da linguagem como um n mero uma letra ou ainda uma string por uma fun o que descarta o argumento a fun o especial identidade a fun o in que constr i um elemento de um tipo de dados indutivo tomando como argumento um elemento do seu functor a fun o out inversa de in e destr i um elemento do tipo de dados indutivo num elemento do seu functor aplicado ao tipo Note se que estas duas ltimas fun es s o parametrizadas no tipo de dados indutivo e consequentemente no seu nico functor mas que gra as s potencialidades do point free pode se abstrair essa parametriza o Mais adiante justificar se a introdu o das fun es in e out Dado o facto de a linguagem de implementa o da ferramenta ser o Haskell estas ideias implementam se muito directamente no tipo de dados indutivo que se segue data PFExp Func String fun es Comp PFExp PFExp composi o Split PFExp PFExp split Prod PFExp PFExp produto Either PFExp PFExp either Sum PFExp PFExp soma projec es Fst primeira projec o Snd segunda projec o injectores InL injector esquerdo InR injector direito Const String fun o constante Id fun o identidade In fun o in Out fun o out 3 2 Limi
56. turas se consiga internalizar e automatizar modos de lidar com tais situa es poupando ao programador esfor os complementares Retome se a an lise a um ramo de uma defini o de uma fun o com o seus lados esquerdo e direito que tem forma lhs rhs aplica se a fun o de convers o PF a ambos os membros e obt m se f e PF lhs g PF rhs Note se que f e g j s o express es point free mas e e el s o vari veis ou pares possivelmente encadeados de vari veis Substituindo se na igualdade lhs rhs e relembrando a sem ntica associada ao par retornado por PF vem 1 fe ge Se e for igual a e o problema est resolvido e vem f g Contudo no caso geral e e e s o diferentes Contudo sabe se que no lado direito de um ramo s podem aparecer vari veis referidas pelo lado esquerdo sem que no entanto haja obrigatoriedade de usar no lado direito todas as vari veis do lado esquerdo isto uma vari vel que ocorre no lado direito tem necessariamente de ocorrer no lado esquerdo mas uma vari vel pode ocorrer no lado esquerdo e n o ocorrer no lado direito Pode se ent o afirmar que o conjunto das vari veis que ocorrem no lado direito est contido no conjunto das vari veis que ocorrem no lado esquerdo Suponha se que era poss vel escrever e como variable Arrange e com variable Arrange uma fun o Atendendo a esta suposi o a igualdade fe ge passa a fe g variable Arrange e que se pode ai
57. ucc plus n Zero b n Succ b Succ plus n Succ b ou ainda trocando a ordem dos ramos da defini o anterior plus Succ plus Zero plus Zero plus Succ n Zero b Succ plus n Zero b a Succ b Succ b a Zero b Zero b n Succ b Succ plus n Succ b As duas ltimas defini es conduzem mesma defini o em point free e esta equiva lente mas diferente da defini o point free gerada pela primeira defini o pointwise da fun o plus Qualquer d vida sugest o ou anomalia bug por favor envie email para pointfrezador sapo pt B Tipo de Dados PFExp module PFExpType PFExp Func Comp Split Prod Either Sum Fst Snd InL InR Const Id In Out instance Eq Show cataPF Data typ data PFExp Comp Split Exp where e to represent point free expressions Func String function PFExp PFExp composition PFExp PFExp split Prod PFExp PFExp product Either PFExp PFExp either Sum PFExp PFExp sum split projections Fst first projection of a pair Snd second projection of a pair either injections InL left injector of co product InR right injector of co product Const String the const function like in Haskell Id the identity function In the in function Out the out function deriving Eq auxP n el e2 simb parA n showsPrec 1 el showString simb showsP
58. ue se cria um argumento que o 1 dos tipos de dados o no Haskell Assim para cada i 1 m 1 Se n zero ent o U 1 2 Se n maior do que zero ent o U Via x X Vin o caso n 1 considerado aqui Em que cada V deriva de T para todo i 1 m e j 1 ni de acordo com as regras que se seguem a Se Ti IndType p p ent o V n o sen o X representa a recursividade do tipo b Se T j pk para algum k 1 1 ent o Vij pk c Se T um construtor de tipos de aridade zero por exemplo Int ent o V j Tij d Se T um produto de tipos de aridade q ent o V um produto de q fac tores em que a cada um deles s o aplicadas as regras 2a a 2d isto Vij Wi j1X x W ijg em que tomando T como Y 1X X Yijq cada Wij n deriva de Y j para todo o h 1 q usando as regras de deriva o 2a a 2d Eis ent o como determinar o functor de um tipo de dados indutivo usando a defini o do tipo Falta pois determinar as fun es in e out que passam respectivamente do func tor para o tipo de dados e vice versa Contudo e porque as fun es s o inversas e os ndices l m e n para todo o 1 m s o finitos tomando as fun es como um con junto de pares ordenados argumento resultado uma das fun es a outra trocando a ordem das componentes para todos os pares do conjunto Ent o analisar se
59. umento na frase anterior refere se ao do construtor HsTyTuple enquanto as componentes referidas est o a outro n vel e dizem respeito s componentes do tipo que um tuplo e representado no tipo HsType HsTyApp HsType HsType aplicac o de tipos o primeiro argumento aplicado ao segundo O exemplo mais usual s o as listas de inteiros com a aplicac o de a Int para se obter o tipo Int HsTyVar HsName vari veis de tipo HsTyCon HsQName construtores de tipo Por exemplo para as listas nativas do Haskell Talvez o leitor j tenha reparado na semelhanca dos nomes HsName e HsQName Na verdade ambos os tipos servem para representar nomes de todo e qualquer elemento no c digo Haskell distinguindo se por o segundo poder representar nomes qualificados ou seja nomes que s o considerados n o globalmente mas apenas no dom nio de nomes do m dulo possivelmente hier rquico indicado como argumento no construtor Qual Tanto para as declara es de tipos de dados indutivos que j se descreveu como para as declara es de inst ncias de classes e de fun es que se descrever o de imediato omitiram se e omitir se o muitos pormenores por forma a abreviar a exposi o Con tudo os mais curiosos podem consultar a documenta o da biblioteca Language Haskell dispon vel online em http www haskell org ghc docs latest html libraries haskell src Language Haskell Syntax html 4 2 Inst ncia de Classe As declara
60. un rio que para cada constante a fixada arbitrariamente d a fun o constante a Este combinador representa se pelo s mbolo e a sua defini o pointwise ala a ou se se preferir a notacao A al Ana Est o assim introduzidos os combinadores mais usuais N o quer isto contudo dizer que este estilo de programa o est limitado aos combinadores apresentados Mais e novos combinadores poder o sempre ser acrescentados para acomodar padr es frequentes de programas e permitindo reduzir os processos de transforma o e ou prova de propriedades Repare se que para combinadores definidos exclusivamente custa de outros com binadores cujas leis j s o conhecidas as respectivas leis surgem rapidamente das leis dos combinadores que lhe servem de base Como este processo se pode repetir poss vel criar combinadores cada vez mais complexos e cujas leis surgem naturalmente Tanto os combinadores apresentados como as fun es b sicas aquelas que se iden tificam pelo respectivo nome incluindo as especiais nomeadamente as projec es e os injectores s o express es funcionais pois quando aplicadas a argumentos comportam se como fun es Como j referido um dos prop sitos do estilo point free a transforma o de progra mas ou seja a substitui o de um programa por um outro equivalente ao original Estes passos ocorrem por aplica o de leis as leis de redu o Devido falta de vari veis estas leis s o mais
61. verter a informa o na forma A Am x B1 Bn em informa o na forma A1xB 4A1xBp2 HAmXxBi1 4AmX Bn Aplicando a distributividade n ria esquerda express o inicial vem Aj x Bi Bn Amx Br Bn Aplicando agora a distributividade n dria direita a cada parcela mais externa vem A x By A x By Am xX Bit Am x Bn que o que se pretendia A transforma o ent o f pfer e NV fein pfema N pfemn NdistR NdistR m parcelas MdistL j out X outB E assim se tem meios para converter uma s rie de defini es pointwise nas suas equivalentes em point free 5 4 Gera o das Fun es in e out Na lei anterior surge a express o outa X outg Por m os elementos em ndice podem ser removidos com o uso de classes De facto tal j sucede na biblioteca Pointless que define uma classe FunctorOf cujas inst ncias t m de declarar o functor do tipo de dados indutivo claro est e as fun es in e out desse tipo indutivo No entanto da responsabilidade do programador criar a inst ncia para cada um dos tipos de dados indutivos que usar Sabe se contudo que um tipo de dados indutivo regular determina univocamente o functor que lhe est associado isto para cada tipo indutivo existe um nico functor Pretende se explorar esta propriedade gerando a partir da defini o de um tipo indutivo e de modo autom tico a inst n
62. where estas instru es neces sitar o de um suporte baseado em teoria de substitui o n o s o ainda tomadas em considera o na teoria apresentada Al m da convers o apresenta se alguma teoria que articulada com a teoria subjacente biblioteca Pointless permite definir automaticamente uma vasta gama de padr es recursivos para a maioria dos tipos de dados indutivos tendo em considera o apenas a defini o destes Ainda neste trabalho complementou se a teoria com uma ferramenta que imple menta uma parte substancial dessa teoria Assim o leitor convidado a experimentar a ferramenta cuja utiliza o descrita no ap ndice A No cap tulo Ideias Em Evolugao 7 fizeram se j algumas sugest es para situa es que n o foram tratadas Assim como trabalho futuro sugere se a extens o da teoria s restantes constru es pointwise acima enumerados o aniquilamento das limita es de implementa o e ainda a investiga o de teoria e respectiva implementa o para se converter defini es point free que s o padr es recursivos mas em que estes n o explicitamente declara dos nas respectivas defini es com padr es recursivos expl citos Agora falando pessoalmente eu o autor n o autor exclusivo pois este trabalho teve contributos significativos do meu orientador e de Alcino Cunha fa o uma avalia o positiva deste projecto com ele adquiri novos conhecimentos sobre a linguagem
Download Pdf Manuals
Related Search