[Haskell-cafe] Transforming a ADT to a GADT

[Florian Lorenzen]

-----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....@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
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Sean Leather]

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]

-----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

- --
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....@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

[Erik Hesselink]

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]

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

[Tsuyoshi Ito]

Dear Florian,

On Fri, Sep 14, 2012 at 6:45 AM, Florian Lorenzen
<florian....@tu-berlin.de> 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

[Erik Hesselink]

On Fri, Sep 14, 2012 at 2:27 PM, Erik Hesselink <hess...@gmail.com> 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)

[ol...@okmij.org]

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.

Let us examine that type:
typecheck :: forall t. Exp -> Maybe (Term t)

Do you really mean that given expression exp, (typecheck exp) should
return a (Maybe (Term t)) value for any t whatsoever? In other words,
you are interested in a type-*checking* problem: given an expression _and_
given a type, return Just (Term t) if the given expression has the given
type. Both expression and the type are the input. Incidentally, this
problem is like `read': we give the read function a string
and we should tell it to which type to parse. If that is what you
mean, then the solution using Typeable will work (although you may
prefer avoiding Typeable -- in which case you should build type
witnesses on your own).

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

Your comment suggests that you mean typecheck exp should return
(Just term) just in case `exp' is well-typed, that is, has _some_
type. The English formulation of the problem already points us towards
an existential. The typechecking function should return (Just term)
and a witness of its type:

typecheck :: Exp -> Sigma (t:Type) (Term t)

Then my

> data TypedTerm = forall ty. (Typ ty) (Term ty)

is an approximation of the Sigma type. As Erik Hesselink rightfully
pointed out, this type does not preclude type transformation
functions. Indeed you have to unpack and then repack. If you
want to know the concrete type, you can pattern-match on the type
witness (Typ ty), to see if the inferred type is an Int, for example.


Chances are that you wanted the following

typecheck :: {e:Exp} -> Result e
where Result e has the type (Just (Term t)) (with some t dependent on
e) if e is typeable, and Nothing otherwise. But this is a dependent
function type (Pi-type). No wonder we have to go through contortions
like Template Haskell to emulate dependent types in Haskell. Haskell
was not designed to be a dependently-typed language.

[José Pedro Magalhães]

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

[Florian Lorenzen]

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

Thanks Oleg for this elaboration. I'm now happy with the solution
involving an existential. I first did not realize that I still could
apply functions of type `Term t -> Term t` as soon as I open the package.

On 09/15/2012 01:02 PM, ol...@okmij.org wrote:
> Florian Lorenzen wrote: Chances are that you wanted the following

>
> typecheck :: {e:Exp} -> Result e where Result e has the type (Just
> (Term t)) (with some t dependent on e) if e is typeable, and
> Nothing otherwise. But this is a dependent function type
> (Pi-type). No wonder we have to go through contortions like
> Template Haskell to emulate dependent types in Haskell. Haskell was
> not designed to be a dependently-typed language.

Yes, this is what I was looking for. I know, Haskell is not
dependently typed. But since many dependently typed idioms (like
printf) can already be expressed using the GHC Haskell type system, I
was wondering if this one was also possible.

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....@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/

iEYEARECAAYFAlBW2YIACgkQvjzICpVvX7alFwCgkS5Gq2CfJqxX5ZV2TJQslSDn
a9IAoJCj3HY5J8kU5T1HcCJGDFbUaLrc
=G/Zf
-----END PGP SIGNATURE-----

[Florian Lorenzen]

-----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
> <hess...@gmail.com> 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....@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-----

[Florian Lorenzen]

-----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
> <florian....@tu-berlin.de

> _______________________________________________ Haskell-Cafe
> mailing list Haskel...@haskell.org

> <mailto:Haskel...@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....@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