Recover type definitions using GHC.Generics

2019-06-27 04:43发布

问题:

Yesterday I took a swing at trying to answer this question about a representation for a datatype. using GHC.Generics. I could recover type definitions for the example problem given, for example, for:

data Artist = Artist Text Genre
data Genre = Jazz | Metal

with the derived Generic instances, default instances for Modelable (the class of things that can recover their type definitions), and a Modelable instance for Text

deriving instance Generic Artist
instance Modelable Artist

deriving instance Generic Genre 
instance Modelable Genre

we can determine that undefined :: Artist has the type of Main.Artist given the preceding type declarations:

data Main.Artist :: *
        Artist Data.Text.Text Main.Genre
data Main.Genre :: *
        Jazz
        Metal

Main.Artist

I represented the type with declarations so that we could also attack recursive data structures like

data ExampleTree = Branch Int ExampleTree ExampleTree | Leaf

Which we can determine is

data Main.ExampleTree :: *
        Branch GHC.Int.Int Main.ExampleTree Main.ExampleTree
        Leaf

Main.ExampleTree

The code I have so far covers all of these cases:

https://gist.github.com/Cedev/9857191

Can we recover the types in a type application?

Right now I have no way to tell the difference between a type applied to two different types, for example [Track] and String ~ [Char]. From the Datatype instance for D I can only recover the outside type, in this case GHC.Types.[], I can't even distinguish the two types.

data Album = Album Artist [Track]
data Track = Track Int String

The following would be acceptable output for the type of an Album, but would be inefficient:

data GHC.Types.[] GHC.Char.Char :: *
        []
        : GHC.Char.Char GHC.Types.[]
data GHC.Types.[] Main.Track :: *
        []
        : Main.Track GHC.Types.[]
data Main.Album :: *
        Album Main.Artist (GHC.Types.[] Main.Track)
data Main.Artist :: *
        Artist Data.Text.Text Main.Genre
data Main.Genre :: *
        Jazz
        Metal
data Main.Track :: *
        Track GHC.Int.Int (GHC.Types.[] GHC.Char.Char)

Main.Album

Since I can't tell the difference between [Track] and String, the closest I can get is something like this, which presumes all []s to contain Track since that's what was encountered first:

data GHC.Types.[] :: *
        []
        : Main.Track GHC.Types.[]
data Main.Album :: *
        Album Main.Artist GHC.Types.[]
data Main.Artist :: *
        Artist Data.Text.Text Main.Genre
data Main.Genre :: *
        Jazz
        Metal
data Main.Track :: *
        Track GHC.Int.Int GHC.Types.[]

Main.Album

Can we recover the type variables in a declaration?

An even better representation would share the definition of []. This would require discovering that [] has kind * -> * and that the type of the first argument of its : constructor comes from the type argument to [].

data GHC.Types.[] :: * -> *
        []
        : (Var 0) GHC.Types.[]
data Main.Album :: *
        Album Main.Artist (GHC.Types.[] Main.Track)
data Main.Artist :: *
        Artist Data.Text.Text Main.Genre
data Main.Genre :: *
        Jazz
        Metal
data Main.Track :: *
        Track GHC.Int.Int (GHC.Types.[] GHC.Char.Char)

Main.Album

Can we recover type definitions for things of kinds other than * and * -> * ?

Would it be possible to recover the definitions for things with more arguments?

data ThreeTuple a b c = ThreeTuple a b c

Which should be for example

data Module.ThreeTuple :: * -> * -> * -> *
        ThreeTuple (Var 0) (Var 1) (Var 2)

Would it be possible to recover the definitions for things with higher order kinds?

data Position f = {
    positionName :: f String
}

data Employee f = {
    employeeName :: f String,
    employeePosition :: f (Position f)
}

Which would be

data Module.Position :: (* -> *) -> *
    Position {
        positionName :: (Var 0) (GHC.Types.[] GHC.Char.Char)
    }

data Module.Employee :: (* -> *) -> *
    Employee {
        employeeName :: (Var 0) (GHC.Types.[] GHC.Char.Char),
        employeePosition :: (Var 0) (Module.Position (Var 0))
    }