Code generation with types For GHC HEAD (7.7.20131005)

code_with_types.hs

-- Code generation with types

-- For GHC HEAD (7.7.20131005)

{-# LANGUAGE
  KindSignatures, DataKinds, PolyKinds, UnicodeSyntax,
  TypeFamilies, UndecidableInstances, TypeOperators, 
  ScopedTypeVariables, ConstraintKinds, FlexibleInstances, 
  MultiParamTypeClasses, FunctionalDependencies, 
  FlexibleContexts, RankNTypes, ImpredicativeTypes, 
  AllowAmbiguousTypes #-}

import qualified Prelude as P

import GHC.TypeLits (Symbol, Nat, natVal, symbolVal, KnownNat, KnownSymbol)

tests = (
  eval (T∷T "foo"),
  eval (T∷T 3),
  eval (T∷T Length) "foo",
  eval (T∷T (Length "foo")),
  eval (T∷T (1 + 2)),
  eval (T∷T ((+) 2)) 1,
  eval (T∷T (+)) 1 2 ∷ P.Integer)

data T (t ∷ k) = T

class Eval (e ∷ k) (v ∷ *) (t ∷ *) | e v → t where
  eval' ∷ proxy e → proxy' v → t

data Length a
instance Eval Length a ([a] → P.Int) where
  eval' _ _ = P.length

instance KnownSymbol s ⇒ Eval (s ∷ Symbol) _x P.String where
  eval' _ _ = symbolVal (T∷T s)

instance KnownNat s ⇒ Eval (s ∷ Nat) _x P.Integer where
  eval' _ _ = natVal (T∷T s)

data a + b
instance P.Num a ⇒ Eval (+) a (a → a → a) where
  eval' _ _ = (P.+)

data a $ b
instance v ~ (a, b) ⇒ Eval ($) v ((a → b) → a → b) where
  eval' _ _ = (P.$)

instance (v ~ (d, e), Eval f d (x → y), Eval a e x) ⇒ Eval (f a) v y where
  eval' _ _ = eval' (T∷T f) (T∷T d) (eval' (T∷T a) (T∷T e))

eval ∷ forall a b c proxy . (Eval a b c) ⇒ proxy a → c
eval e = eval' e (T∷T b)

foo :: forall a . P.Show a ⇒ P.String
foo = P.show (P.Nothing ∷ P.Maybe a)