GADT question

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

GADT question

oleg-7

John Meacham wrote:

>  data Type = ForAll [TyVar] Rho   -- Forall type
>           | Fun    Type Type      -- Function type
>           | TyCon  TyCon          -- Type constants
>           | TyVar  TyVar          -- Always bound by a ForAll

> with the three synonyms and their constraints being

> type Sigma = Type
> type Rho   = Type       -- No top-level ForAll
> type Tau   = Type       -- No ForAlls anywhere

> I would like the type system to distinguish the three types and enforce
> their properties.

Perhaps the enclosed code might be of help. Tests:

        test1 = TyCon "Int"
        *Forall> :t test1
        test1 :: Type FANil

        test2 = Forall ["a"] (Fun (TyVar "a") (TyVar "a"))
        *Forall> :t test2
        test2 :: Type FATop

        -- Inferred type!
        test3 = Fun test2 test1
        *Forall> :t test3
        test3 :: Type FASomewhere

        test3' = Fun test1 test1
        *Forall> :t test3'
        test3' :: Type FANil

        test4 = Forall ["b"] test3
        *Forall> :t test4
        test4 :: Type FATop

        test4' = Forall ["b"] test2 -- Error!
        No instance for (RhoC FATop)
        arising from use of `Forall' at /tmp/m.hs:43:9-14

That is, in test4, the second argument of Forall is not of the type
rho! Typeclasses would work too. I'm lacking a good example to show
off this machinery...


{-# OPTIONS -fglasgow-exts #-}

module Forall where

data FANil
data FATop
data FASomewhere

type Id = String

type Tau = Type FANil

data Type a where
    Forall :: (RhoC a) => [Id] -> Type a -> Type FATop
    Fun    :: (FAMerge a b c) => Type a -> Type b -> Type c
    TyCon  :: Id -> Type FANil
    TyVar  :: Id -> Type FANil

type Sigma a = Type a
--type (RhoC a) => Rho a =   Type a -- I wish that worked...

class RhoC a
instance RhoC FANil
instance RhoC FASomewhere

class FAMerge a b c | a b -> c
instance FAMerge FANil FANil FANil
instance FAMerge FANil FASomewhere FASomewhere
instance FAMerge FANil FATop FASomewhere
instance FAMerge FATop       a FASomewhere
instance FAMerge FASomewhere a FASomewhere

test1 = TyCon "Int"
test2 = Forall ["a"] (Fun (TyVar "a") (TyVar "a"))
test3 = Fun test2 test1
test3' = Fun test1 test1

-- I guess we need to hide the data constructors of Type and use
-- functions like rho, fun, tycon, etc. to construct the values of
-- Type
rho :: (RhoC a) => Type a -> Type a
rho = id

test4 = Forall ["b"] test3
-- The following is error!
--test4' = Forall ["b"] test2
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

RE: GADT question

Simon Peyton Jones
 
| I would like the type system to distinguish the three types and
enforce
| their properties. so far, I have come up with the following:
|
|
| data Sigma
| data Tau
| data Rho
|
| data Type a where
|     ForAll :: [Id] -> Type Rho -> Type Sigma
|     Fun :: Type a -> Type a -> Type a
|     TyCon :: TyCon -> Type Tau
|     TyVar :: TyVar -> Type Tau

It looks as if you want a kind of subtyping relationship, so that Tau <
Rho < Sigma.  The standard way to achieve that is using polymorphism
(see, for example, papers about FFI to object-oriented languages)

data Sigma a = S a
data Rho a = R a
data Tau = Tau

data Type a where
|     ForAll :: [Id] -> Type (Sigma (Rho a)) -> Type (Sigma b)
|     Fun :: Type a -> Type a -> Type a
|     TyCon :: TyCon -> Type (Sigma (Rho Tau))
|     TyVar :: TyVar -> Type (Sigma (Rho Tau))

I'm not sure if this would work.

Simon
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe