issue with GADT

Stream: new members

[Alok Singh]

I'm reading https://acatalepsie.fr/posts/overloading-lambda.html and found

{-# LANGUAGE GADTs #-}

data Flow a b where
  -- just a wire
  Id :: Flow a a
  -- putting two boxes one after the other
  Seq :: Flow a b -> Flow b c -> Flow a c
  -- putting two boxes one next to the other
  Par :: Flow a b -> Flow c d -> Flow (a, c) (b, d)
  -- box that duplicates its input
  Dup :: Flow a (a, a)
  -- box that gets rid of its input
  Void :: Flow a ()
  -- box that projects on first input
  Fst :: Flow (a, b) a
  -- box that projects on second input
  Snd :: Flow (a, b) b
  -- finally, we embed any pure function into a box
  Embed :: (a -> b) -> Flow a b

Encoding this as

inductive Flow (a b:Type) where
  /-- just a wire --/
  | Id : Flow a a
  /-- putting two boxes one after the other --/
  | Seq : Flow a b -> Flow b c -> Flow a c
  /-- putting two boxes one next to the other --/
  | Par : Flow a b -> Flow c d -> Flow (a, c) (b, d)
  /-- box that duplicates its input --/
  | Dup : Flow a (a, a)
  /-- box that gets rid of its input --/
  | Void : Flow a ()
  /-- box that projects on first input --/
  | Fst : Flow (a, b) a
  /-- box that projects on second input --/
  | Snd : Flow (a, b) b
  /-- finally, we embed any pure function into a box --/
  | Embed : (a -> b) -> Flow a b

gives error

inductive datatype parameter mismatch
  a
expected
  b

[Daniel Weber]

What are the types of a, b? They definitely shouldn't be Types

[Daniel Weber]

You can do this:

inductive Flow : {α β : Type} → α → β → Type 1 where
  /-- just a wire --/
  | Id (a : α) : Flow a a
  /-- putting two boxes one after the other --/
  | Seq : Flow a b → Flow b c → Flow a c
  /-- putting two boxes one next to the other --/
  | Par : Flow a b -> Flow c d -> Flow (a, c) (b, d)
  /-- box that duplicates its input --/
  | Dup : Flow a (a, a)
  /-- box that gets rid of its input --/
  | Void : Flow a ()
  /-- box that projects on first input --/
  | Fst : Flow (a, b) a
  /-- box that projects on second input --/
  | Snd : Flow (a, b) b
  /-- finally, we embed any pure function into a box --/
  | Embed : (a -> b) -> Flow a b

[Eric Wieser]

Or maybe they should be types but (a , b) should actually be a × b?

[Daniel Weber]

Yes, reading that website maybe they should be

[Daniel Weber]

In that case this works:

inductive Flow : Type → Type → Type 1 where
  /-- just a wire --/
  | Id : Flow a a
  /-- putting two boxes one after the other --/
  | Seq : Flow a b -> Flow b c -> Flow a c
  /-- putting two boxes one next to the other --/
  | Par : Flow a b -> Flow c d -> Flow (a × c) (b × d)
  /-- box that duplicates its input --/
  | Dup : Flow a (a × a)
  /-- box that gets rid of its input --/
  | Void : Flow a Unit
  /-- box that projects on first input --/
  | Fst : Flow (a × b) a
  /-- box that projects on second input --/
  | Snd : Flow (a × b) b
  /-- finally, we embed any pure function into a box --/
  | Embed : (a → b) → Flow a b

[Shreyas Srinivas]

Perhaps this helps : https://lean-lang.org/functional_programming_in_lean/dependent-types/indexed-families.html

[Shreyas Srinivas]

Polymorphic inductive types take type arguments. For instance, List takes an argument that determines the type of the entries in the list, and Except takes arguments that determine the types of the exceptions or values. These type arguments, which are the same in every constructor of the datatype, are referred to as parameters.

Arguments to inductive types need not be the same in every constructor, however. Inductive types in which the arguments to the type vary based on the choice of constructor are called indexed families, and the arguments that vary are referred to as indices

[Shreyas Srinivas]

Also the structure you are implementing is some variation on the Arrow typeclass. In mathlib you will find a lawful version of Arrows. I think they call it Freyd category or comma category