Combine Full/:-> as their own datatype

[Icelandjack]

I haven't seen these used at the value level at all:

newtype Full a = Full { result :: a }
newtype a :-> b = Partial (a -> b)

instead the term types are gotten with:

type family   Denotation sig
type instance Denotation (Full a)    = a
type instance Denotation (a :-> sig) = a -> Denotation sig

Could Full and :-> be defined as

data A a where
  Full  :: a      -> A a
  (:->) :: a -> b -> A a

type family   
  Denotation (sig :: A Type) :: Type where
  Denotation (Full a)    = a
  Denotation (a :-> sig) = a -> Denotation sig

Everything seems to work fine.

AST gets the following kind:

data AST :: (A a -> Type) -> (A a -> Type) where
  Sym  :: dom sig -> AST dom sig
  (:$) :: AST dom (a :-> sig) -> AST dom (Full a) -> AST dom sig

[emilaxelsson]

That's a good idea. You're welcome to submit a patch.

Syntactic currently builds fine on GHC 7.6, but it would be fine to only support 7.8 and upwards if needed.

[Icelandjack]

Is it possible that the result and a -> b are used somewhere (another package?) so I don't know if this would break something — Why were = Full { result :: a } and = Partial (a -> b) added to begin with?

data Full a
data a :-> b

More importantly I need a name for A! :) maybe Sig for signature?

data Sig :: Type -> Type where
  Full  :: a      -> A a
  (:->) :: a -> b -> A a

Cons

It would actually change the type of every symbol domain, and break anything that makes assumptions about their kind,

-- Now this is
--   NUM :: Sig Type -> Type

data NUM :: Type -> Type where
  Num :: Int -> NUM (Full Int)

Show1 NUM, Eq1 NUM, ... no longer work...

Show1 :: (Type -> Type) -> Constraint
  Eq1 :: (Type -> Type) -> Constraint

Pros

With the new design we can use deeply embed our universe of types:

data TY = I8 | I32

data NUM' :: Sig TY -> Type where
  Num8  :: Int8 -> NUM' (Full I8)
  Num32 :: Int  -> NUM' (Full I32)
  Add   :: NUM' (a :-> a :-> Full a)

[emilaxelsson]

No, there are no value-level uses of Full and :-> AFAIR. Whenever a signature is needed at the value level, the Denotation type family is used to convert it to function form.

Sig seems like a good name for A :+1:

Overall I think your suggestion looks like an improvement.

[Icelandjack]

Does this change make sense to you?

data Sig :: Type -> Type where
  Full  :: a          -> Sig a
  (:->) :: a -> Sig a -> Sig a

---

The previous definition of Sig was too big, it allows this domain to have a bogus semantic value that can never be constructed using Sym / :$

data U = MkU

data Mon :: Sig U -> Type where
  Mempty  :: Mon (Full MkU)
  Mappend :: Mon (MkU :-> 'True :-> "hi")

since the kind of type Fn2 a b c = a :-> b :-> Full c is

Fn2 :: a -> b -> c -> Sig a

Its kind is now

Fn2 :: a -> a -> a -> Sig a

and the only valid definition of Mon is

data Mon :: Sig U -> Type where
  Mempty  :: Mon (Full MkU)
  Mappend :: Mon (MkU :-> MkU :-> Full MkU)

[Icelandjack]

Now we can also lift the the mutually-recursive Expression and Statement domains from A Generic Abstract Syntax Model for Embedded Languages and give them a more descriptive kind

data Prog = E Type | S

data ExprDom :: Sig Prog -> Type where
  NumSym  :: Int -> ExprDom (Full (E Int))
  AddSym  :: ExprDom (E Int :-> E Int :-> Full (E Int))
  ExecSym :: Var -> ExprDom (S :-> Full (E a))

data StmtDom :: Sig Prog -> Type where
  AssignSym :: Var -> StmtDom (E a :-> Full S)
  SeqSym    :: StmtDom (S :-> S :-> Full S)

[emilaxelsson]

@Icelandjack wrote:

Does this change make sense to you?

Yes, it looks like the right design. I'd be happy to accept a PR if you go through with this (and no unforeseen complications pop up).

[Icelandjack]

I'll go through it, it's also nice to get rid of the existential: now a signature is simply the non-empty list!

data Sig a = Full a | a :-> Sig a

data NonEmpty a = a :| [a]

[emwap]

I think that would be taking the simplification one step too far. Shouldn't it still be

data Sig a = Full a | b :-> Sig a

Am I missing something?

[Icelandjack]

What do we gain with that existential variable? It allows us to define function-valued symbols with any domain but with no way to interpret them with AST, i.e.

data POO :: Sig Type -> Type where
  MkPOO :: POO ("hi" :-> Full Int)
  -- Kind error
  MkSYM :: POO (Full "hi")

a :: AST POO ("hi" :-> Full Int)
a = Sym MkPoo

-- Kind error
b = (:$) a

---

If we parametrise AST by the constructors we see that it constrains the first arguments of Full, :-> to have the same kind

-- AST :: (a -> b) -> (a -> b -> b) -> (b -> Type) -> (b -> Type)

data AST full arr dom a where
  Sym  :: dom a -> AST full arr dom a
  (:$) :: AST full arr dom (a `arr` b) 
       -> AST full arr dom (full a) 
       -> AST full arr dom b

Partially applying it to Full tells us that (:->) :: a -> Sig a -> Sig a

AST Full :: (a -> Sig a -> Sig a) -> (Sig a -> Type) -> (Sig a -> Type)

[emwap]

Ah, sorry, I was thinking it was the type, not the kind. Please, disregard my comment.

[Icelandjack]

I'm working on it, there are some difficulties

[Icelandjack]

If I restrict AST :: (Sym Type -> Type) -> (Sym Type -> Type) it is ready to merge, but then we lose the ability to talk about universes of types.

[emilaxelsson]

I suppose you mean AST :: (Sig Type -> Type) -> (Sig Type -> Type) ?

That's a good start! If/when the problem gets solved we can go the whole way to kind-polymorphic signatures.

[Icelandjack]

I did mean that, I think I'll do that but I'm curious...

When do we need Domain and Internal separately from when we need AST _ _? The reason I ask is that the kind of Domain a :: Sig u -> Type and the kind of Internal a :: u but the u effectively needs to be existential(?) since it needs to be the same kind and it is independent of a and is not reflected in Type.

We could generate the AST directly:

class Syntactic (a :: Type) where
  type ASTify a :: Type
  desugar :: a -> ASTify a
  sugar   :: ASTify a -> a  

Things like SyntacticN that currently uses Domain, Internal can now be written as

-- instance {-# OVERLAPPING #-} (Syntactic f, Domain f ~ sym, fi ~ AST sym (Full (Internal f))) => SyntacticN f fi
instance {-# OVERLAPPING #-} (Syntactic f, ASTify f ~ ASTF sym f', fi ~ ASTF sym f') => SyntacticN f fi where
  desugarN :: f -> ASTF sym f'
  desugarN = desugar

  sugarN :: ASTF sym f' -> f
  sugarN = sugar

-- instance {-# OVERLAPPING #-} (Syntactic a, Domain a ~ sym, ia ~ Internal a, SyntacticN f fi) => SyntacticN (a -> f) (AST sym (Full ia) -> fi)
instance {-# OVERLAPPING #-} (Syntactic a, ASTify a ~ ASTF sym ia, SyntacticN f fi) => SyntacticN (a -> f) (ASTF sym ia -> fi) where
  desugarN :: (a -> f) -> (ASTF sym ia -> fi)
  desugarN f = desugarN . f . sugar

  sugarN :: (ASTF sym ia -> fi) -> (a -> f) 
  sugarN f = sugarN . f . desugar

It simplifies some things

-- resugar :: (Syntactic a, Syntactic b, Domain a ~ Domain b, Internal a ~ Internal b) => a -> b
resugar :: (ASTify a ~ ASTify c, Syntactic a, Syntactic c) => a -> c
resugar = sugar . desugar

but would instances for a -> b require a type family? This makes me think I'm going in the wrong direction

type family
  ASTifyArr a b where
  ASTifyArr (ASTF dom a) (ASTF dom b) = ASTF dom (a -> b)

instance Syntactic (a -> b) where
  type ASTify (a -> b) = ASTifyArr (ASTify a) (ASTify b)

Any insights?

[emilaxelsson]

I don't think we ever need to talk about Domain separately, but we do need Internal. See e.g. the types of eval and value.

Would this work with your approach? Would the of eval become this:

eval :: (Syntactic a, ASTify a ~ Data ia) => a -> ia

The problem with -> indeed seems a bit ugly. You'd need to do the same for tuples of different widths.

Otherwise I like the idea. It would avoid exposing the Domain family to the user, which is currently sometimes a problem in error messages.

[oliver-batchelor]

Hi @Icelandjack what was the main sticking point here after all?

I'm going to have a play around - I wonder if it's not possible to use the restricted AST in places where it only makes sense that way. i.e. seems to make sense to restrict thing like 'eval' to work on concrete types?

[oliver-batchelor]

Or - I guess there's something missing - for things like 'eval' with a closed universe there needs to be some way of specifying a mapping from the closed universe to concrete types...

[oliver-batchelor]

This compiles (https://github.com/emilaxelsson/syntactic/pull/31) without changing the design, classes like Syntactic and Eval are Sig Type -> Type restricted.

I think there should be a simple enough way to wrap a symbol type in a closed universe to one on Haskell types in order to use it with Eval or Syntactic etc? I'll have a play around and see..