A complete first-class description of datatypes?

[VictorTaelin]

Gabriel, I'm wondering if you're aware of any first-class description of datatypes. I don't mean the encoding themselves, but an actual representation of the types per see. For example, the description of Bool would somehow encode the information in data Bool = True | False and, with it, one could create both constructors generically. The description of List would be a function Description -> Description, which could, again, be used to create the cons Type and nil Type constructors. I guess you get what I'm talking about. Is there any reference for that?

[Gabriella439]

I guess my question is: what could the first-class description have that the Boehm-Berarducci encoding wouldn't?

For example, the Boehm-Berarducci encoding of the type Bool is:

∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool

... which has the exact same information as data Bool = True | False. Same thing for lists:

  ∀(a : *)
→ ∀(List : *)
→ ∀(Cons : ∀(head : a) → ∀(tail : List) → List)
→ ∀(Nil : List)
→ List

[VictorTaelin]

Ah, the point is that such a first class description could be used like that:

True = DeriveConstructor 0 BoolT

That would return the Boehm-Berarducci-encoded constructor. Or, for example:

DepthTreeInt = DeriveDepth (TreeT IntT)

DeriveDepth, on that case, returns a function that takes the depth of any ADT given its description. If I'm not mistaken you can't create such a DeriveDepth function using the Boehm-Berarducci type itself, you need some kind of description of the ADT. So, basically, not an alternative to the encoding, just a convenience to derive sctructural functions for it automatically. Which makes programming on Morte easier. I remember having read a paper about something like that, but it was loong ago...

[Gabriella439]

What would be the type of DeriveConstructor, though?

DeriveDepth is pretty easy: you just encode every type description as a record where one field is the depth and then DeriveDepth just extracts that field.

[VictorTaelin]

I'm not sure what you're saying, but DeriveDepth would for example return the length function in the case of a List... makes sense that DeriveConstructor couldn't have a type... which kinda sucks, so we can't have first-class generics like we can on the untyped λ-calculus...

Edit: actually I think it could have a type, yes, let me try something

[VictorTaelin]

Posted this on S.O., I wonder if you have any clue whether something like that can be typed? I'm having some trouble with the fact it is supposed to return different types and I'm not sure if I can't get it right or if it is just impossible. Do you know?

[Gabriella439]

I believe it's not possible in System Fw. For anything where the type of the result doesn't change (like depth) then it's easy, but if the type of the result changes then you run into issues.

[VictorTaelin]

Hey it is actually possible as long as * : *, but I think you wouldn't be very happy with that, right?

[Gabriella439]

Yeah, that won't type check in System Fw (or any other consistent type system) because once the type system accepts * : * then you can make anything type check by creating a value of type ∀(a : *) → a that loops infinitely

[VictorTaelin]

How would that value look like?

[Gabriella439]

I don't understand the details myself, but I believe that this paper provides the "simplest" explanation of how to construct such a value: https://www.cs.cmu.edu/~kw/scans/hurkens95tlca.pdf

[VictorTaelin]

Hey I found another way to make that work, you just have to give a type to □, like, □:● where ● itself has no type. Then this code does it:

Data

∀ (D: □) ->
∀ (A: □) ->
∀ (M: □) ->
∀ (data: (A -> D)) ->
∀ (add: (M -> A -> A)) ->
∀ (zer: A) ->
∀ (mul: (D -> D) -> M -> M) ->
∀ (one: M) ->
D

Data.Type

λ (data: #Data ) ->
(data
*
(* -> *)
(* -> *)
(λ (DT:(* -> *)) -> ∀ (T:*) -> (DT T))
(λ (CT:(* -> *)) -> λ (E:(* -> *)) -> λ (T:*) -> ((CT T) -> (E T)))
(λ (T:*) -> T)
(λ (FT:((* -> *) -> * -> *)) -> λ (E:(* -> *)) -> λ (T:*) -> ((FT (λ (x:*) -> x) T) -> (E T)))
(λ (T:*) -> T))

Nat.Data

λ (D: *) ->
λ (A: *) ->
λ (M: *) ->
λ (data: A -> D) ->
λ (add: M -> A -> A) ->
λ (zer: A) ->
λ (mul: (D -> D) -> M -> M) ->
λ (one: M) ->
(data 
  (add (mul (λ (nat:D) -> nat) one) 
  (add one zer)))

Here, Data is the type of ADT descriptions, Data.Type is a function of type Data -> * which returns a type given an ADT. We can then apply (#Data.Type #Nat.Data ) and that normalizes to ∀ (a:*) -> (a -> a) -> a -> a! It even works for nested types like lists of nats and so on. With that, our user could write something like Type (Add (Mul Rec One) (Add One Zero)) instead of ∀ (a:*) -> (a -> a) -> a -> a.!

That might sound worse but we could use that same expression to derive constructors, equality, functor, all at language level. Also if we had a syntax sugar for strings, we could have type (data "Succ Rec | Zero"), where data parses a string to get an ADT, using dependent types to fail at compile time if it isn't a valid syntax. Basically a template system but with just functions.

[VictorTaelin]

Just to be clear, I know the same can be achieved by features outside the language such as Annah, but the reason I insist on this so much is that the core principle of functional languages is that, whenever you find something complicated enough, you abstract over it with functions. All those: equality, constructors, zip, map, fold, match, read, show, serialize, deserialize, and possibly more, are difficult to write by hand, but can be mechanically generated from a datatype description. So why, in 2016, should a programmer be writing them manually? I find it a shame that generic programming is so complex in Haskell and often needs outside help ("templates"). Hopefully that will not be the case with CoC, and we'll be able to derive tons of stuff from just a single ADT definition.

[puffnfresh]

@MaiaVictor (* : *) gives Russell's paradox:

https://gist.github.com/copumpkin/2631136

[VictorTaelin]

Hey cool, that is quite short. I wonder how is that in Morte.

[Gabriella439]

@MaiaVictor Also, if this sort of thing interests you, you might find this paper interesting: http://web.cs.ucla.edu/~palsberg/paper/popl16-full.pdf