Extensión Haskell PolyKinds y familias de tipos.

Estoy trabajando en las familias de tipos en Haskell para profundizar en este tema y estoy tratando de usar tipos polimórficos y familias de tipos al mismo tiempo.

Por ejemplo, al comienzo del archivo se tienen las siguientes extensiones de lenguaje (hay más en el archivo que no se mostrarán aquí):

{-# LANGUAGE TypeFamilies, StandaloneKindSignatures, RankNTypes, PolyKinds, DataKinds, TypeOperators, TypeApplications, KindSignatures, ScopedTypeVariables, UndecidableInstances, MultiParamTypeClasses, AllowAmbiguousTypes #-}

Luego estoy usando tipos polimórficos en la declaración de tipos:

data Proxy (a :: k) = Proxy

lo cual funciona bien. Pero cuando intento usarlos dentro de familias de tipos con una definición más compleja:

type family PK (a :: k) :: Type where PK Int = Char

GHC arroja un error:

• Se esperaba un tipo ‘k’, pero ‘Int’ tiene tipo ‘*’ • En el primer argumento de ‘PK’, a saber ‘Int’ En la declaración de la familia de tipos para ‘PK’.

¿Hay alguna solución para eso? La versión de GHC es 8.10.7. Gracias de antemano por cualquier idea o ayuda.

davy.ai

July 11, 2023 at 5:23 pm

Parece que el problema es que GHC espera un tipo k en la declaración de la familia de tipos para PK, pero Int tiene tipo * (que es el tipo para tipos concretos). Una posible solución sería hacer de PK una función a nivel de tipo en lugar de una familia de tipos, de la siguiente manera:

type family CharIfInt (a :: k) :: Type where
  CharIfInt Int = Char

type PK (a :: k) = CharIfInt a

Aquí, definimos una función a nivel de tipo CharIfInt que toma cualquier argumento de tipo k y devuelve Char si el argumento es Int, y de lo contrario produce un error de tipo. Luego, usamos esta función para definir PK como un sinónimo de tipo que especializa el argumento a a Int si es Int, y de lo contrario produce un error de tipo.

Este enfoque debería permitirte usar tipos polimórficos y familias de tipos al mismo tiempo en tu código Haskell.

Answer

davy.ai

July 11, 2023 at 5:23 pm
Parece que el problema es que GHC espera un tipo k en la declaración de la familia de tipos para PK, pero Int tiene tipo * (que es el tipo para tipos concretos). Una posible solución sería hacer de PK una función a nivel de tipo en lugar de una familia de tipos, de la siguiente manera:
```
type family CharIfInt (a :: k) :: Type where
  CharIfInt Int = Char

type PK (a :: k) = CharIfInt a
```
Aquí, definimos una función a nivel de tipo CharIfInt que toma cualquier argumento de tipo k y devuelve Char si el argumento es Int, y de lo contrario produce un error de tipo. Luego, usamos esta función para definir PK como un sinónimo de tipo que especializa el argumento a a Int si es Int, y de lo contrario produce un error de tipo.

Este enfoque debería permitirte usar tipos polimórficos y familias de tipos al mismo tiempo en tu código Haskell.

Comments are closed.

es.davy.ai

¿Tienes una pregunta?

Extensión Haskell PolyKinds y familias de tipos.

Answer

davy.ai