Transforming a ADT to a GADT

older
Re: [Haskell-cafe] Transforming a...

Florian Lorenzen

14 Sep 2012 14 Sep '12

6:45 a.m.

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 Hello cafe, I have a question wrt. to GADTs and type families in GHC (7.6.1). I'd like to transform a value of an ADT to a GADT. Suppose I have the simple expression language

...

data Exp = Lit Int > | Succ Exp > | IsZero Exp > | If Exp Exp Exp

and the GADT

...

data Term t where > TLit :: Int -> Term Int > TSucc :: Term Int -> Term Int > TIsZero :: Term Int -> Term Bool > TIf :: Term Bool -> Term ty -> Term ty -> Term ty

that encodes the typing rules. Now, I'd like to have a function

...

typecheck :: Exp -> Maybe (Term t) > typecheck exp = <...>

that returns the GADT value corresponding to `exp' if `exp' is type correct. I found a solution at http://okmij.org/ftp/tagless-final/TypecheckedDSLTH.hs but this has as type (slightly adapted)

...

typecheck :: Exp -> Maybe TypedTerm

with

...

data TypedTerm = forall ty. (Typ ty) (Term ty) > data Typ ty = TInt Int | TBool Bool

That is, the GADT value is hidden inside the existential and cannot be unpacked. Therefore, I cannot write a type preserving transformation function like

...

transform :: Term t -> Term t

that gets the result of the `typecheck' function as input. The solution mentioned above uses Template Haskell to extract the `Term t' type from the existential package and argues that type errors cannot occur during splicing. Is there a possibility to avoid the existential and hence Template Haskell? Of course, the result type of typecheck depends on the type and type correctness of its input. My idea was to express this dependency by parameterizing `Exp' and using a type family `ExpType' like:

...

typecheck :: Exp e -> Maybe (Term (ExpType e)) > typecheck (ELit i) = Just (TLit i) > typecheck (ESucc exp1) = case typecheck exp1 of > Nothing -> Nothing > Just t -> Just (TSucc t) > <...>

with

...

data TEXP = L | S TEXP | IZ TEXP | I TEXP TEXP TEXP -- datakind >

...
data Exp (e::TEXP) where > ELit :: Int -> Exp L > ESucc :: Exp e1 -> Exp (S e1) > EIsZero :: Exp e1 -> Exp (IZ e1) > EIf :: Exp e1 -> Exp e2 -> Exp e3 -> Exp (I e1 e2 e3)

It seems to me that `ExpType' then would be a reification of the type checker for `Exp' at the type level. But I did not know how to define it. Does it make sense at all? Is it possible in GHC? All the examples on the net I looked at either start with the GADT right away or use Template Haskell at some point. So, perhaps this `typecheck' function is not possible to write in GHC Haskell. I very much appreciate any hints and explanations on this. Best regards, Florian - -- Florian Lorenzen Technische Universität Berlin Fakultät IV - Elektrotechnik und Informatik Übersetzerbau und Programmiersprachen Sekr. TEL12-2, Ernst-Reuter-Platz 7, D-10587 Berlin Tel.: +49 (30) 314-24618 E-Mail: florian.lorenzen@tu-berlin.de WWW: http://www.user.tu-berlin.de/florenz/ -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.11 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://www.enigmail.net/ iEYEARECAAYFAlBTCr8ACgkQvjzICpVvX7ZfTgCeOPflPtaEW/w1McjYWheaRaqq oUQAnRXSrGP3se+3oiI3nnd+B/rK8yx8 =X1hR -----END PGP SIGNATURE-----

Show replies by date

Sean Leather

14 Sep 14 Sep

8:01 a.m.

On Fri, Sep 14, 2012 at 12:45 PM, Florian Lorenzen wrote:

...

I'd like to transform a value of an ADT to a GADT. Suppose I have the simple expression language

...
data Exp = Lit Int > | Succ Exp > | IsZero Exp > | If Exp Exp Exp

and the GADT

...
data Term t where > TLit :: Int -> Term Int > TSucc :: Term Int -> Term Int > TIsZero :: Term Int -> Term Bool > TIf :: Term Bool -> Term ty -> Term ty -> Term ty

that encodes the typing rules.

Now, I'd like to have a function

...
typecheck :: Exp -> Maybe (Term t) > typecheck exp = <...>

that returns the GADT value corresponding to `exp' if `exp' is type correct.

It's not pretty, but it should still be safe... import Control.Applicative import Unsafe.Coerce tcInt :: Exp -> Maybe (Term Int) tcInt (Lit i) = pure (TLit i) tcInt (Succ e) = TSucc <$> tcInt e tcInt (If c e1 e2) = TIf <$> tcBool c <*> tcInt e1 <*> tcInt e2 tcInt _ = empty tcBool :: Exp -> Maybe (Term Bool) tcBool (IsZero e) = TIsZero <$> tcInt e tcBool (If c e1 e2) = TIf <$> tcBool c <*> tcBool e1 <*> tcBool e2 tcBool _ = empty typecheck :: Exp -> Maybe (Term t) typecheck e = forget <$> tcInt e <|> forget <$> tcBool e where forget :: Term a -> Term b forget = unsafeCoerce Regards, Sean

Florian Lorenzen

8:13 a.m.

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 Dear Sean, thanks for your solution. It in the documentation of unsafeCoerce it says: "It [unsafeCoerce] is generally used when you want to write a program that you know is well-typed, but where Haskell's type system is not expressive enough to prove that it is well typed." May I conclude that the (GHC) Haskell type system is not powerful enough to type such a typecheck function? Best regards, Florian On 09/14/2012 02:01 PM, Sean Leather wrote:

...

On Fri, Sep 14, 2012 at 12:45 PM, Florian Lorenzen wrote:

I'd like to transform a value of an ADT to a GADT. Suppose I have the simple expression language

...
data Exp = Lit Int > | Succ Exp > | IsZero Exp > | If Exp Exp Exp

and the GADT

...
data Term t where > TLit :: Int -> Term Int > TSucc :: Term Int -> Term Int > TIsZero :: Term Int -> Term Bool > TIf :: Term Bool -> Term ty -> Term ty -> Term ty

that encodes the typing rules.

Now, I'd like to have a function

...
typecheck :: Exp -> Maybe (Term t) > typecheck exp = <...>

that returns the GADT value corresponding to `exp' if `exp' is type correct.

It's not pretty, but it should still be safe...

import Control.Applicative import Unsafe.Coerce

tcInt :: Exp -> Maybe (Term Int) tcInt (Lit i) = pure (TLit i) tcInt (Succ e) = TSucc <$> tcInt e tcInt (If c e1 e2) = TIf <$> tcBool c <*> tcInt e1 <*> tcInt e2 tcInt _ = empty

tcBool :: Exp -> Maybe (Term Bool) tcBool (IsZero e) = TIsZero <$> tcInt e tcBool (If c e1 e2) = TIf <$> tcBool c <*> tcBool e1 <*> tcBool e2 tcBool _ = empty

typecheck :: Exp -> Maybe (Term t) typecheck e = forget <$> tcInt e <|> forget <$> tcBool e where forget :: Term a -> Term b forget = unsafeCoerce

Regards, Sean

- -- Florian Lorenzen Technische Universität Berlin Fakultät IV - Elektrotechnik und Informatik Übersetzerbau und Programmiersprachen Sekr. TEL12-2, Ernst-Reuter-Platz 7, D-10587 Berlin Tel.: +49 (30) 314-24618 E-Mail: florian.lorenzen@tu-berlin.de WWW: http://www.user.tu-berlin.de/florenz/ -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.11 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://www.enigmail.net/ iEYEARECAAYFAlBTH10ACgkQvjzICpVvX7ZIVACdEPtbEHbVeQcdgzQTanVkpeKq 8QsAn3b774JsVyMMVc1lIN2rFlTVheQD =zgOc -----END PGP SIGNATURE-----

Erik Hesselink

8:27 a.m.

On Fri, Sep 14, 2012 at 2:01 PM, Sean Leather wrote:

...

On Fri, Sep 14, 2012 at 12:45 PM, Florian Lorenzen wrote:

...
I'd like to transform a value of an ADT to a GADT. Suppose I have the simple expression language

...
data Exp = Lit Int > | Succ Exp > | IsZero Exp > | If Exp Exp Exp

and the GADT

...
data Term t where > TLit :: Int -> Term Int > TSucc :: Term Int -> Term Int > TIsZero :: Term Int -> Term Bool > TIf :: Term Bool -> Term ty -> Term ty -> Term ty

that encodes the typing rules.

Now, I'd like to have a function

...
typecheck :: Exp -> Maybe (Term t) > typecheck exp = <...>

that returns the GADT value corresponding to `exp' if `exp' is type correct.

It's not pretty, but it should still be safe...

import Control.Applicative import Unsafe.Coerce

tcInt :: Exp -> Maybe (Term Int) tcInt (Lit i) = pure (TLit i) tcInt (Succ e) = TSucc <$> tcInt e tcInt (If c e1 e2) = TIf <$> tcBool c <*> tcInt e1 <*> tcInt e2 tcInt _ = empty

tcBool :: Exp -> Maybe (Term Bool) tcBool (IsZero e) = TIsZero <$> tcInt e tcBool (If c e1 e2) = TIf <$> tcBool c <*> tcBool e1 <*> tcBool e2 tcBool _ = empty

typecheck :: Exp -> Maybe (Term t) typecheck e = forget <$> tcInt e <|> forget <$> tcBool e where forget :: Term a -> Term b forget = unsafeCoerce

I don't think this is safe. What will happen if you evaluate typecheck (Lit 1) :: Maybe (Term Bool) In general, I think you have to work inside an existential. So you hide the type of the parsed Term inside an existential. If you want to apply functions to this Term, you unpack, call the function, and repack. I don't think there's a way around this, since the type parameter to Term _is_ existential. You know there is some type, but you don't know what it is. If you make it polymorphic, the _called_ can choose it, which is the opposite of what you want. Erik

Sean Leather

8:42 a.m.

On Fri, Sep 14, 2012 at 2:27 PM, Erik Hesselink wrote:

...

I don't think this is safe. What will happen if you evaluate typecheck (Lit 1) :: Maybe (Term Bool)

Indeed! Silly me. Caught by the lure again. Thanks. Regards, Sean

Erik Hesselink

9:22 a.m.

On Fri, Sep 14, 2012 at 2:27 PM, Erik Hesselink wrote:

...

In general, I think you have to work inside an existential. So you hide the type of the parsed Term inside an existential. If you want to apply functions to this Term, you unpack, call the function, and repack.

Maybe I should expand what I mean by this. Let's say you have: data SomeTerm where SomeTerm :: Term a -> SomeTerm Your typecheck function goes: typecheck :: Exp -> SomeTerm and you want to apply: transform :: Term t -> Term t You should do something like: f (SomeTerm t) = SomeTerm (transform t) Or, more generally: onSomeTerm :: (forall t. Term t -> Term t) -> SomeTerm -> SomeTerm onSomeTerm f (SomeTerm t) = SomeTerm (f t) Erik

Florian Lorenzen

17 Sep 17 Sep

4:05 a.m.

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 Thanks Erik. This made the issue clear to me. Best regards, Florian On 09/14/2012 03:22 PM, Erik Hesselink wrote:

...

On Fri, Sep 14, 2012 at 2:27 PM, Erik Hesselink wrote:

...
In general, I think you have to work inside an existential. So you hide the type of the parsed Term inside an existential. If you want to apply functions to this Term, you unpack, call the function, and repack.

Maybe I should expand what I mean by this. Let's say you have:

data SomeTerm where SomeTerm :: Term a -> SomeTerm

Your typecheck function goes:

typecheck :: Exp -> SomeTerm

and you want to apply:

transform :: Term t -> Term t

You should do something like:

f (SomeTerm t) = SomeTerm (transform t)

Or, more generally:

onSomeTerm :: (forall t. Term t -> Term t) -> SomeTerm -> SomeTerm onSomeTerm f (SomeTerm t) = SomeTerm (f t)

Erik

- -- Florian Lorenzen Technische Universität Berlin Fakultät IV - Elektrotechnik und Informatik Übersetzerbau und Programmiersprachen Sekr. TEL12-2, Ernst-Reuter-Platz 7, D-10587 Berlin Tel.: +49 (30) 314-24618 E-Mail: florian.lorenzen@tu-berlin.de WWW: http://www.user.tu-berlin.de/florenz/ -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.11 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://www.enigmail.net/ iEYEARECAAYFAlBW2bgACgkQvjzICpVvX7Zr3QCfbIqkX9WqM69NLyk98aqyNcYe RrUAniGndhj9OTl9XIoUBC/hoBI1lwML =hReY -----END PGP SIGNATURE-----

Tsuyoshi Ito

14 Sep 14 Sep

9:11 a.m.

Dear Florian, On Fri, Sep 14, 2012 at 6:45 AM, Florian Lorenzen wrote:

...

Now, I'd like to have a function

...
typecheck :: Exp -> Maybe (Term t) > typecheck exp = <...>

that returns the GADT value corresponding to `exp' if `exp' is type correct.

If you can add “deriving Typeable” to Term and you are fine with a less general type typecheck :: Typeable t => Exp -> Maybe (Term t) then you can use Data.Typeable.cast. ----- {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE GADTs #-} module ADTToGADT where import Control.Applicative import Data.Typeable data Exp = Lit Int | Succ Exp | IsZero Exp | If Exp Exp Exp data Term t where TLit :: Int -> Term Int TSucc :: Term Int -> Term Int TIsZero :: Term Int -> Term Bool TIf :: Term Bool -> Term ty -> Term ty -> Term ty deriving Typeable typecheck :: Typeable t => Exp -> Maybe (Term t) typecheck (Lit i) = cast $ TLit i typecheck (Succ e) = castTerm $ TSucc <$> typecheck e typecheck (IsZero e) = castTerm $ TIsZero <$> typecheck e typecheck (If c e1 e2) = TIf <$> typecheck c <*> typecheck e1 <*> typecheck e2 castTerm :: (Typeable a, Typeable b) => Maybe (Term a) -> Maybe (Term b) castTerm Nothing = Nothing castTerm (Just t) = cast t ----- Best regards, Tsuyoshi

José Pedro Magalhães

16 Sep 16 Sep

7:45 a.m.

Hi Florian, Will this do? class Tc a where tc :: Exp -> Maybe (Term a) instance Tc Int where tc (Lit i) = return (TLit i) tc (Succ i) = tc i >>= return . TSucc tc (IsZero i) = Nothing tc e = tcIf e instance Tc Bool where tc (Lit i) = Nothing tc (Succ i) = Nothing tc (IsZero i) = tc i >>= return . TIsZero tc e = tcIf e tcIf :: (Tc a) => Exp -> Maybe (Term a) tcIf (If c e1 e2) = do c' <- tc c e1' <- tc e1 e2' <- tc e2 return (TIf c' e1' e2') Cheers, Pedro On Fri, Sep 14, 2012 at 11:45 AM, Florian Lorenzen < florian.lorenzen@tu-berlin.de> wrote:

...

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1

Hello cafe,

I have a question wrt. to GADTs and type families in GHC (7.6.1).

I'd like to transform a value of an ADT to a GADT. Suppose I have the simple expression language

...
data Exp = Lit Int > | Succ Exp > | IsZero Exp > | If Exp Exp Exp

and the GADT

...
data Term t where > TLit :: Int -> Term Int > TSucc :: Term Int -> Term Int > TIsZero :: Term Int -> Term Bool > TIf :: Term Bool -> Term ty -> Term ty -> Term ty

that encodes the typing rules.

Now, I'd like to have a function

...
typecheck :: Exp -> Maybe (Term t) > typecheck exp = <...>

that returns the GADT value corresponding to `exp' if `exp' is type correct.

I found a solution at http://okmij.org/ftp/tagless-final/TypecheckedDSLTH.hs but this has as type (slightly adapted)

...
typecheck :: Exp -> Maybe TypedTerm

with

...
data TypedTerm = forall ty. (Typ ty) (Term ty) > data Typ ty = TInt Int | TBool Bool

That is, the GADT value is hidden inside the existential and cannot be unpacked. Therefore, I cannot write a type preserving transformation function like

...
transform :: Term t -> Term t

that gets the result of the `typecheck' function as input.

The solution mentioned above uses Template Haskell to extract the `Term t' type from the existential package and argues that type errors cannot occur during splicing.

Is there a possibility to avoid the existential and hence Template Haskell?

Of course, the result type of typecheck depends on the type and type correctness of its input.

My idea was to express this dependency by parameterizing `Exp' and using a type family `ExpType' like:

...
typecheck :: Exp e -> Maybe (Term (ExpType e)) > typecheck (ELit i) = Just (TLit i) > typecheck (ESucc exp1) = case typecheck exp1 of > Nothing -> Nothing > Just t -> Just (TSucc t) > <...>

with

...
data TEXP = L | S TEXP | IZ TEXP | I TEXP TEXP TEXP -- datakind >

...
data Exp (e::TEXP) where > ELit :: Int -> Exp L > ESucc :: Exp e1 -> Exp (S e1) > EIsZero :: Exp e1 -> Exp (IZ e1) > EIf :: Exp e1 -> Exp e2 -> Exp e3 -> Exp (I e1 e2 e3)

It seems to me that `ExpType' then would be a reification of the type checker for `Exp' at the type level. But I did not know how to define it. Does it make sense at all? Is it possible in GHC?

All the examples on the net I looked at either start with the GADT right away or use Template Haskell at some point. So, perhaps this `typecheck' function is not possible to write in GHC Haskell.

I very much appreciate any hints and explanations on this.

Best regards,

Florian

- -- Florian Lorenzen

Technische Universität Berlin Fakultät IV - Elektrotechnik und Informatik Übersetzerbau und Programmiersprachen

Sekr. TEL12-2, Ernst-Reuter-Platz 7, D-10587 Berlin

Tel.: +49 (30) 314-24618 E-Mail: florian.lorenzen@tu-berlin.de WWW: http://www.user.tu-berlin.de/florenz/ -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.11 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://www.enigmail.net/

iEYEARECAAYFAlBTCr8ACgkQvjzICpVvX7ZfTgCeOPflPtaEW/w1McjYWheaRaqq oUQAnRXSrGP3se+3oiI3nnd+B/rK8yx8 =X1hR -----END PGP SIGNATURE-----

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Florian Lorenzen

17 Sep 17 Sep

4:12 a.m.

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 José, it occurs to me that with this solution, I always have to prescribe the type as in

...

tc (Succ (Lit 5)) :: Maybe (Term Int)

Otherwise, I obtain the message Ambiguous type variable `a0' in the constraint: (Tc a0) arising from a use of `tc' But as Oleg already pointed out, I want to have a value `Just term :: Maybe (Term t)' if the input is well-typed for some type which I don't know. Best regards, Florian On 09/16/2012 01:45 PM, José Pedro Magalhães wrote:

...

Hi Florian,

Will this do?

class Tc a where tc :: Exp -> Maybe (Term a)

instance Tc Int where tc (Lit i) = return (TLit i) tc (Succ i) = tc i >>= return . TSucc tc (IsZero i) = Nothing tc e = tcIf e

instance Tc Bool where tc (Lit i) = Nothing tc (Succ i) = Nothing tc (IsZero i) = tc i >>= return . TIsZero tc e = tcIf e

tcIf :: (Tc a) => Exp -> Maybe (Term a) tcIf (If c e1 e2) = do c' <- tc c e1' <- tc e1 e2' <- tc e2 return (TIf c' e1' e2')

Cheers, Pedro

On Fri, Sep 14, 2012 at 11:45 AM, Florian Lorenzen mailto:florian.lorenzen@tu-berlin.de> wrote:

Hello cafe,

I have a question wrt. to GADTs and type families in GHC (7.6.1).

I'd like to transform a value of an ADT to a GADT. Suppose I have the simple expression language

...
data Exp = Lit Int > | Succ Exp > | IsZero Exp > | If Exp Exp Exp

and the GADT

...
data Term t where > TLit :: Int -> Term Int > TSucc :: Term Int -> Term Int > TIsZero :: Term Int -> Term Bool > TIf :: Term Bool -> Term ty -> Term ty -> Term ty

that encodes the typing rules.

Now, I'd like to have a function

...
typecheck :: Exp -> Maybe (Term t) > typecheck exp = <...>

that returns the GADT value corresponding to `exp' if `exp' is type correct.

I found a solution at http://okmij.org/ftp/tagless-final/TypecheckedDSLTH.hs but this has as type (slightly adapted)

...
typecheck :: Exp -> Maybe TypedTerm

with

...
data TypedTerm = forall ty. (Typ ty) (Term ty) > data Typ ty = TInt Int | TBool Bool

That is, the GADT value is hidden inside the existential and cannot be unpacked. Therefore, I cannot write a type preserving transformation function like

...
transform :: Term t -> Term t

that gets the result of the `typecheck' function as input.

The solution mentioned above uses Template Haskell to extract the `Term t' type from the existential package and argues that type errors cannot occur during splicing.

Is there a possibility to avoid the existential and hence Template Haskell?

Of course, the result type of typecheck depends on the type and type correctness of its input.

My idea was to express this dependency by parameterizing `Exp' and using a type family `ExpType' like:

...
typecheck :: Exp e -> Maybe (Term (ExpType e)) > typecheck (ELit i) = Just (TLit i) > typecheck (ESucc exp1) = case typecheck exp1 of Nothing -> Nothing > Just t -> Just (TSucc t) > <...>

with

...
data TEXP = L | S TEXP | IZ TEXP | I TEXP TEXP TEXP -- datakind

...
data Exp (e::TEXP) where > ELit :: Int -> Exp L > ESucc :: Exp e1 -> Exp (S e1) > EIsZero :: Exp e1 -> Exp (IZ e1) > EIf :: Exp e1 -> Exp e2 -> Exp e3 -> Exp (I e1 e2 e3)

It seems to me that `ExpType' then would be a reification of the type checker for `Exp' at the type level. But I did not know how to define it. Does it make sense at all? Is it possible in GHC?

All the examples on the net I looked at either start with the GADT right away or use Template Haskell at some point. So, perhaps this `typecheck' function is not possible to write in GHC Haskell.

I very much appreciate any hints and explanations on this.

Best regards,

Florian

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org mailto:Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

- -- Florian Lorenzen Technische Universität Berlin Fakultät IV - Elektrotechnik und Informatik Übersetzerbau und Programmiersprachen Sekr. TEL12-2, Ernst-Reuter-Platz 7, D-10587 Berlin Tel.: +49 (30) 314-24618 E-Mail: florian.lorenzen@tu-berlin.de WWW: http://www.user.tu-berlin.de/florenz/ -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.11 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://www.enigmail.net/ iEYEARECAAYFAlBW24UACgkQvjzICpVvX7bWZACfVWRiNrJVl/ue5sk/AFsAK36m zeUAniWoGahDymxAqkBK6JWQ5jNzDR6f =FRcI -----END PGP SIGNATURE-----

4629

Age (days ago)

4632

Last active (days ago)

List overview

Download

9 comments

5 participants

participants (5)

Erik Hesselink
Florian Lorenzen
José Pedro Magalhães
Sean Leather
Tsuyoshi Ito