Sum of `Type -> Type`

Stream: new members

[Nicolas Rolland]

Are there standard constructor like Sum for Type -> Type or for more general kinds ?

In Init/Core.lean we have

/--
`Sum α β`, or `α ⊕ β`, is the disjoint union of types `α` and `β`.
An element of `α ⊕ β` is either of the form `.inl a` where `a : α`,
or `.inr b` where `b : β`.
-/
inductive Sum (α : Type u) (β : Type v) where
  /-- Left injection into the sum type `α ⊕ β`. If `a : α` then `.inl a : α ⊕ β`. -/
  | inl (val : α) : Sum α β
  /-- Right injection into the sum type `α ⊕ β`. If `b : β` then `.inr b : α ⊕ β`. -/
  | inr (val : β) : Sum α β

@[inherit_doc] infixr:30 " ⊕ " => Sum

Alternatively is it better to go through categorical non sense : we can inherit a sum for Type ⥤ Type through the monoidal properties of Type (where are those derivations ?)

I am trying to recreate the classic higher order "toolkit" for defining data types, to define various folds as categorical constructions

[Eric Wieser]

I don't understand your question; are you looking for docs#Sigma ? For (Type -> Type) ⊕ (Type -> Type)?

[Nicolas Rolland]

Eric Wieser said:

are you looking for docs#Sigma ? For (Type -> Type) ⊕ (Type -> Type)?

Not quite.

Going the Type -> Type way, that would simply be

inductive Sum' (f : Type u -> Type x) (g : Type u -> Type w) (a : Type u) where
  | inl' (val : f a) : Sum' f g a
  | inr' (val : g a) : Sum' f g a

The ordinary Sum being a particular case with constant f mapping to a and g mapping to b
That can help to define say List a as a least fix point of ListF r = ( ctt 1 ⊕ a * _ ) r where we combine type constructors (and prove that they are functor later on)

But we can also look at the structure on the Type category and combine functors type through the bunch of extra categorical properties of Type, deriving the functor sum with

/--
When `C` is any category, and `D` is a monoidal category,
the functor category `C ⥤ D` has a natural pointwise monoidal structure,
where `(F ⊗ G).obj X = F.obj X ⊗ G.obj X`.
-/
instance functor_category_monoidal : monoidal_category (C ⥤ D) := ...

In that case ListF r = ( ctt 1 ⊕ a * _ ) rwould immediately be a functor Type ⥤ Type

I wonder if there's anything agreed upon on those line or should I do my own combinator library..

[Eric Wieser]

Your Sum' f g a is the same thing as Sum (f a) (g a):

example (f : Type u -> Type x) (g : Type u -> Type w) (a : Type u) :
  Sum' f g a ≃ Sum (f a) (g a) where
    toFun
    | .inl' l => .inl l
    | .inr' l => .inr l
    invFun
    | .inl l => .inl' l
    | .inr l => .inr' l
    left_inv x := by cases x <;> rfl
    right_inv x := by cases x <;> rfl

[Nicolas Rolland]

indeed. this pointwise business is very trivial. i would prefer to not define my own combinators

[Eric Wieser]

Is this sufficient for you?

def Function.Sum (f : Type u -> Type x) (g : Type u -> Type w) : Type u → Type _ :=
  fun a => f a ⊕ g a

[Nicolas Rolland]

My question is : Is this Function.Sum in a standard library ?

My issue is code reuse, for me, and for other people who might use my stuff.
You can imagine if there was different versions of, say, Functor, doing the same things. and people building on top of different versions.

[Yaël Dillies]

This is docs#Sum

[Nicolas Rolland]

Not quite, it's an indexed/pointwise version of docs#Sum.
This can be used as a "toolkit" to define data type.

For instance in haskell

newtype K a x = K a deriving Functor             -- K for konstant
{- fmap _ (K a) = K a -}
newtype I x = I x deriving Functor               -- I for identity
{- fmap k (I x) = I (k x) -}
newtype P f g x=P(f x,g x) deriving Functor --P for product
 {- will give (Functor f, Functor g) => Functor (P f g), such that
   fmap k (P (f x, g x)) = P (fmap k f x, fmap k g x) -}
newtype S f g x = S (Either (f x) (g x))         -- S for sum
instance (Functor f, Functor g) => Functor (S f g) where
  fmap k (S (Left  f x))  = S (Left  (fmap k f x))
  fmap k (S (Right g x))  = S (Right (fmap k g x))

allows to view integer binary tree as the least fixed point of the endofunctor

type TreeF = S (K Int) (P I I)

type Tree = Mu TreeF

etc..

[Mario Carneiro]

you will have difficulty defining least fixed point in that way

[Mario Carneiro]

more generally, lean does not promote "point free" style as much as haskell, plus it doesn't have as many restrictions regarding functions at the kind level, so if you want a lambda you can just use a lambda

[Mario Carneiro]

you could write TreeF much more clearly as

def TreeF (A : Type) := Int ⊕ (A × A)

instead of writing combinatory logic

[Nicolas Rolland]

As a data type I think it would be unsafe inductive, but I imagine I can Church encode it.

Good to keep in mind for the style.

[Mario Carneiro]

the more idiomatic way to write Tree itself would be

inductive Tree where
  | leaf : Int → Tree
  | node : Tree → Tree → Tree

and you can use metaprogramming to prove that this type is the LFP of TreeF

[Nicolas Rolland]

Oh I see ! Can I then extract some TreeF (and then build a fold) for this using metaprogramming ?

(I remember there is some trick to extract TreeF from Tree in Haskell)

Having combinators helps to derive the map of morphisms instead of manually writing them.
Maybe there is some clever way to get them back as well using metaprogramming ?

I imagine I should look at "metaprogramming in lean" for this LFP and the rest ?

[Mario Carneiro]

some of the details for this are worked out in our QPF paper but admittedly it's somewhat complicated to automatically extract functorial structure from arbitrary inductives

[Nicolas Rolland]

For reference to haskellers or otherwise,

To recover the underlying functor of a regular inductive data type in haskell, it pattern matches on the typed generic representation.
This Generic mechanism is part of the trusted core and is at work in deriving Generic.

I imagine a similar mechanism could be part of a standard metaprogramming library in Lean ?

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Scratch where

import Data.Functor.Compose as C
import Data.Functor.Constant
import Data.Functor.Identity
import GHC.Generics as G

type family FG r a where
  FG _ (U1) = Constant ()
  FG r (K1 _ x) = Distrib r x
  FG r ((:+:) f g) = ((:+:) (FG r f) (FG r g))
  FG r ((:*:) f g) = ((:*:) (FG r f) (FG r g))
  FG r (D1 _ k) = FG r k
  FG r (M1 _ _ k) = FG r k

type family Distrib r f where
  Distrib l l = Identity
  Distrib r (f a) = Compose f (Distrib r a)
  Distrib _ o = Constant o

data Rose a = Leaf | Rose a [Rose a]
  deriving (Generic)

type ToFunc a = FG a (Rep a)

data Fix f = Fix (f (Fix f))

type Fix' f0 = Fix (ToFunc f0)

*Scratch> :kind! Fix' (Rose Int)
Fix' (Rose Int) :: *
= Fix (Constant () :+: (Constant Int :*: Compose [] Identity))