Thank you. Yeah those 'record type’s are what I’d call “practically indistinguishable” from class decls: a bunch of extra attributes that means the methods are more than ordinary functions.
What I do see in those docos is
the special module application
open Monoid {{...}} public
This will bring into scope
mempty : ∀ {a} {A : Set a} {{_ : Monoid A}} → A
_<>_ : ∀ {a} {A : Set a} {{_ : Monoid A}} → A → A → A
The open is ML-style overloading: bring into scope a specific instance. Any use of mempty within that scope is to be the Set instance irrespective of whether that’s the type demanded by the consumer. Needs a lot of bondage-and-discipline bureaucracy, is what I hear.
The “defined by hand” further down the page using Monoid.mempty is a nod to OOP style.
(Haskell-style typeclasses also need some level of bureaucracy. Particularly explicit signatures to prod the compiler into selecting the right instance. So I’m not saying better nor worse, just a different/incompatible mindset.)
Record types are essentially just syntactic sugar for a data type, along with a module of the same name, containing the fields and any definitions declared/opened. So while using record types is the typical way of doing type classes à la Haskell, it can be done with types defined other ways.
class declarations don’t define types, they define type classes (in the narrow, programming specific sense). Records define types, and in a dependent type theory, types can model type classes (in a general sense). So yeah, when you use record types to do what class declarations do, you get something “practically indistinguishable.”
Set is the type (or “sort”) of (“small”) types, analogous to Haskell’s *.
open Monoid {{...}} public brings mempty and _<>_ into scope with the instance argument unresolved. So if you have a file with the docs’ Monoid definition, open Monoid {{...}} public, a definition of Nat : Set, 0 : Nat and _+_ : Nat → Nat → Nat, and only the following instance declaration for Monoid Nat:
Then Agda would complain about overlapping instances, unless ran with --overlapping-instances. Off the top of my head, I don’t remember what Agda does here with overlapping instances enabled (and I don’t have access to an Agda compiler at the moment).
However, if instead of defining +-Monoid and *-Monoid within an instance block, they were just defined at the top level, then one could do open Monoid {{+-Monoid}} resulting in mempty : Nat and _<>_ : Nat → Nat → Nat in scope. One could also do x = 2 <> 3 where open Monoid {{+-Monoid}} to scope it just to the definition of x. Or there’s (assuming open Monoid {{...}}, or open Monoid {{...}} public in a module that’s been opened:
Thank you for confirming @knottio, that’s the main takeway from that part of the discussion. IOW no functional/Dependently-typed language has invented something radically different from typeclasses. (We might nit-pick with what you say, that these days Haskell’s classes are in fact types: GHCi’s :info Eq says type Eq :: * -> Constraint.)
Errk. That is maximally confusing. I did see that Agda maintains an (infinite) hierarchy of types rather than Haskell’s Type-in-Type. Looking again at that doco page, I see both it : ∀ {a} {A : Set a} ... and elem : {A : Set} {{eqA : Eq A}} .... That seems an inconsistent usage of Set. Ok I’ll stop trying to understand Agda. Is all dependent typing as confusing as that?
Those aren’t merely overlapping instances, they’re identical instances, which are to be rejected in all cases. Then the only recourse in Haskell is to define some newtype over Nat, and make that an instance of Monoid. Haskell doesn’t allow private instances. (There are from time to time requests for local instances or some such. Nobody’s been able to give a coherent explanation for how that interacts with the global typeclass mechanism.)
Very likely I was/am failing to understand. It seemed to me that “defined by hand” was binding local mempty to a specific instance of Monad, not leaving it overloadable. For example, binding to +-Monad rather than *-Monad. That is, treating +-Monad as an object (in the OOP sense), and drawing some specific overloading of mempty from it, rather than resolving to the instance determined from type inference.
So I’m left puzzled: if Agda’s instance resolution is always type-driven, what’s the point of giving a name to an instance (like +-Monad)? Where would you use that name? Can you use that name to override what type inference would otherwise do?
However, when you use the more generalized aspects of record types, you can do more than what Haskell’s class declarations can do. You can, for example, bundle the type classes’ laws within the type class, so that an instance of the type class includes not just the functions, but proof the functions satisfy the desired laws. That is radically different.
The choice to use “Set” is unfortunate, although it can now be renamed. Recent projects in Agda tend to use “Type” instead.
Type-in-type with dependent types gives rise to what is more or less Russell’s paradox (“the set of all sets that aren’t members of themselves”). Stratified universes are common in set theory to resolve Russell’s paradox, and Agda does the analogous thing for its type theory.
Set by itself is syntactic sugar for Set 0, so it is universe polymorphic since it’s parameterized by the Level variable a, whereas elem is not, since the {A : Set} is sugar for {A : Set 0}.
I suspect the documentation and syntax of Agda hasn’t had much feedback from people trying to learn Agda without prior knowledge of some dependent type theory, or at the very least such individuals were learning dependent type theory from other sources in tandem.
Right, so Agda won’t be able to resolve an instance of Monoid Nat. Having both declared as instances with the same scope isn’t useful (as far as I’m aware). However, they can be declared in separate modules, and careful control of opening those modules is one way of being able to choose which instances will get resolved.
Yep! Since the “type constraints” in Agda are actually just types and their inhabitants, the instance resolution is used to resolve a specific inhabitant of a type, to be used as an argument to a function (or module)
The argument can be passed explicitly instead of relying on instance resolution, e.g. for a function f : {{Monoid Nat}} → Nat → Nat → Nat, one could call f {{+-Monoid}} 2 3 to have the function use 0 as the unit, and addition as the operation, or f {{*-Monoid}} 2 3 to use 1 and multiplication instead.
And for a module parameterized by an instance (such as the Monoid module), explicitly passing an instance lets you open the module with that specific instance applied. e.g. open Monoid {{+-Monoid}} brings into scope mempty and _<>_ with the instance partially applied, giving them the types Nat and Nat → Nat → Nat respectively.
Additionally, you can write a function that takes a Monoid Nat explicitly, and then pass either +-Monoid or *-Monoid as you would any other argument.
Hmm interesting. When T-in-T was introduced into Haskell, the powers-that-be were aware of the risk of undecidability. But figured there were already plenty of ways for the type/class system to be undecidable, so it wasn’t making anything worse. OTOH that was before Dependent Typing. OTOOH, a major power-that-be had already written their thesis all about DT in Haskell. So I’m bemused.
If I might critique that of which I know nothing, that seems totally cr*p design: any constructor can be partially applied. In higher-order typing, aren’t there contexts (constructor classes?) where you want (unapplied) Set to be an argument to a fancy doo-hickey?
I have looked at endless tutorials on Dependent Type theory. They’ve failed to resonate with me in any usable way. (Or perhaps I mean I’ve failed to resonate with them.) Then I was reading the Agda docos in the hope of more practical material. Clearly I’m mentally incompetent. Wise of me to just keep away from Haskell here on.
That sounds dangerously like ‘orphan instances’. Nobody’s been able to bring an example where that causes actual incoherence/segfaults. OTOH it regularly gives perplexing behaviour. so GHC gives warnings if it suspects that’s happening. The language standard is written on the basis all instances are visible at all times.
What you go on to say “The argument can be passed explicitly instead of relying on instance resolution, …” sounds like
a) at least a “radically different” way to use typeclasses/instances [**], even if a fairly familiar way to declare them;
b) an excellent source for hard-to diagnose overloading behaviour; in particular
c) an awkward way to interact with Agda’s equivalent of Functional Dependencies (presumably type-level functions needing instance resolution).
Thank you for all your help (trying to) unconfuse me. I suspect I’m a hopeless case.
[**] Addit: we-ell you could contrive Haskell to kinda sorta mimic that usage. A module with the NatPlusMonad instance; a module with NatTimesMonad. Be very careful to never import them both into the same place. That’ll be really difficult because of the likelihood of transitive imports.
Does Dependent Haskell embody “another” type system? Or is it an (allegedly) easier to grok mechanism to replace FunDeps, (Assoc) Type Families, awkwardness with signatures needing binding and scoping of tyvars? [Genuine questions: I don’t know.]
Or is there to be a two-tier Haskell?: those writing the compiler and core libraries speak the language of the priesthood; stupid Haskellers (like me) merely use those libraries, aren’t expected to write infrastructure-level code, so don’t need to deal with exotic types. [I have a wee suspicion they’ll still see obscure type-riddled error messages.] To repeat a point from above: it’ll all be out of sight behind extensions.
Does Dependent Haskell embody “another” type system?
Here’s a simpler question: do dependent types require “another” type system?
So if Haskell is (currently) “poor man’s Agda”…I would say yes.
Before TypeInType arrived in GHC, kinds were the “type” of types and sorts were the “type” of kinds. So in addition to the type and kind systems, GHC also had a sort system.
As for Agda:
I have a wee suspicion they’ll still see obscure type-riddled error messages.
It won’t only be error messages:
# ghci -XHaskell2010
GHCi, version 9.8.2: https://www.haskell.org/ghc/ :? for help
ghci> :t case getChar of IO a -> a
<interactive>:1:17: error: [GHC-76037]
Not in scope: data constructor ‘IO’
ghci>
ghci> :i IO
type IO :: * -> *
newtype IO a -- None of
= GHC.Types.IO (GHC.Prim.State# GHC.Prim.RealWorld -- this should
-> (# GHC.Prim.State# GHC.Prim.RealWorld, a #)) -- be visible in
-- Defined in ‘GHC.Types’ -- Haskell-2010 mode
instance Monoid a => Monoid (IO a) -- Defined in ‘GHC.Base’
instance Semigroup a => Semigroup (IO a) -- Defined in ‘GHC.Base’
instance Applicative IO -- Defined in ‘GHC.Base’
instance Functor IO -- Defined in ‘GHC.Base’
instance MonadFail IO -- Defined in ‘Control.Monad.Fail’
instance Monad IO -- Defined in ‘GHC.Base’
ghci>
(a : Level) → Set a is what Set would be if it wasn’t overridden by syntactic sugar. So you could give that a name, e.g. Set' = (a : Level) → Set a and use Set', but people generally just write (a : Level) → Set a out in full, especially since you often need to give the level a name, anyway. Regardless, I don’t think I’ve ever written a type where I could actually use Set', since usually you want something like (a : Level) → Set a → ... not ((a : Level) → Set a) -> ... and Set' → ... would be the latter.
I suspect the learning curve for dependent types is fairly front-loaded; requiring you to learn a lot very early on, with seemly no gain, then suddenly new concepts come much more easily when presented using the dependently typed fundamentals. Seems similar to category theory in that regard. How true that is remains to be seen.
I’m not familiar with the intricacies of orphan instances. From what I skimmed from the Haskell wiki, it seems it isn’t applicable in Agda because Agda has private instances, and has --no-qualified-instances which allows using a module with a public instance without Agda considering the instance for resolution.
I suppose it would make more sense to talk about parametric vs ad-hoc polymorphism here. In Haskell, if you wanted to do “type classes” parametrically, you would do e.g.:
-- defining Monoid for parametric polymorphism
data Monoid' a = Monoid' { mempty' :: a, mappend' :: a -> a -> a }
-- defining a new function parameterized by a Monoid
mconcat' :: Monoid' a -> [a] -> a
mconcat' mon = foldr (mappend' mon) (mempty' mon)
-- defining an "instance" of Monoid
listMonoid :: Monoid' [a]
listMonoid = Monoid' [] (++)
-- using a function with Monoid parametrically
x = mconcat' listMonoid [ [ 0 ] ]
vs. the ad-hoc polymorphism of e.g.:
-- defining Monoid for ad-hoc polymorphism
class Monoid a where
mempty :: a
mappend :: a -> a -> a
-- defining new function with a Monoid constraint
mconcat :: Monoid a => [a] -> a
mconcat = foldr mappend mempty
-- defining an instance of Monoid
instance Monoid [a] where
mempty = []
mconcat = (++)
-- using a function with Monoid ad-hoc
x = mconcat [ [ 0 ] ]
But in Agda, when defining Monoid, you don’t have to make a choice of parametric vs ad-hoc; you can make the choice when using Monoid, instead:
-- defining a Monoid for ad-hoc AND parametric polymorphism
record Monoid (a : Set) : Set where
field
mempty : a
mappend : a -> a -> a
open Monoid {{...}} public
-- defining a new function parameterized by a Monoid, as an instance argument
mconcat : {a} -> {{Monoid a}} -> List a -> a
mconcat = foldr mappend mempty
-- defining an instance of Monoid
instance
listMonoid : {a} -> Monoid (List a)
listMonoid = record { mempty = []; mappend = _++_ }
-- using a function with Monoid ad-hoc
xAdhoc = mconcat [ [ 0 ] ]
-- using a function with Monoid parametrically
xPara = mconcat {{listMonoid}} [ [ 0 ] ]
With this one definition, you can use Monoid ad-hoc by using it like you would a type class in Haskell, e.g. mconcat [ [ 0 ] ] (assuming an appropriate instance available), or you can use it like you would in the parametric Haskell version above (e.g. Haskell: mconcat listMonoid [ [ 0 ] ]) except the Monoid argument is surrounded by double braces, e.g. mconcat {{listMonoid}} [ [ 0 ] ].
So it’s less “using typeclasses in a radically different way” and more “using parametric polymorphism when it’s more appropriate than ad-hoc, without requiring separate ad-hoc and parametric implementations”.
I don’t know what “overloading behaviour” refers to here.
Reminds me of type level programming in TypeScript. Some libraries will use black magic advanced type definitions to better constrain valid vs invalid inputs; often at the cost of impenetrable type errors. Similarly, in Agda, inspecting type holes in an algebra 101 proof involving the stdlib rational numbers can easily result in displaying a single type take takes up your whole screen. Although I’ve heard that’s been improved a bit recently.
Likewise, adding more data redundancy means more data, and more data means more data corruption. Hence why I don’t backup any of my data: it increases the likelihood of corruption! Instead, I store my data long term with maximal compression to reduce its footprint.
That was written 2014, rather a long time after Oleg’s work, which included IIRC a Sudoku solver written entirely within the type system, chiefly to demonstrate how compile-time is Turing-complete. I am not claiming that work is easy to follow.
Then I’m unimpressed by what I’ve seen so far of Dependent Haskell (or Agda), because it seems to add an awful lot of ugly syntax, to achieve no more than I (or rather Oleg) can already [**]. Note Oleg originally used only FunDeps, not even Type Families, nor DataKinds.
This wasn’t specific to GHC. Haskell 98 Language report, section 4.1.1 Kinds
unlike types, kinds are entirely implicit and are not a visible part of the language.
So it’s the language that already has a kind system (and even more shadowy sort system). Then to answer the question at hand: no, Dependent Haskell isn’t adding “another” layer. What GHC provided was to make it more visible so you can write kind signatures. (They’re useful documentation, but not essential: the compiler can infer kinds from the type sig. You can set an option in Hugs to see Kind signatures.)
Distinguishing terms vs types vs kinds is what allows punning, including that kind * is distinct from term (*). And this doesn’t give rise to ambiguity because to the left of :: is a different namespace to its right (is different to the right of a :: nested on rhs of ::). It all works rather elegantly IMHO. DataKinds and then Type-in-type is the slippery slope to: allowing types in terms with no syntactic herald is an act of vandalism.
[**] Beware a few type-level extensions were taken out of GHC sometime after 2006, meaning you nowadays are forced to use the ugly syntax.
Here’s one difference between kinds in Haskell 98 and (pre-TypeInType) GHC:
So the fragment of a kind system that was in Haskell 98 was getting closer and closer to being another fully-formed “type” system in GHC. And if it weren’t for the TypeInType extension, the same would have eventually happened for the fragment of the sort system that was in Haskell 98.
It’s a perpetual cycle:
SystemN for "types"N is developed;
Over time, systemN acquires fragments of systemN +1 to accommodate more features for "types"N.
As a result of that ongoing expansion, the problems that had appeared in systemN begin to re-appear in systemN +1.
(Increment N by one, then go back to step 1.)
So how many more times does this cycle have to be repeated before everyone realises that the result after each time will always be the same - to infinity and beyond?
Yes, fair comment. Haskell doesn’t support private instances in any way. Even if you tried to contrive them with cunning use of the module/import system, the compiler would probably defeat you. (“orphan instances” is the effect of applying within one module an instance which the compiler wouldn’t choose for exactly the same code if it could see all instances where this module is going to get imported into.)
I’m pretty sure that won’t scale:
do notation insists on the standard names for Monadic operations;
classes are arranged in hierarchies, with Laws to bind between them. (class Semigroup a => Monoid a ..., class Applicative m => Monad m, class Functor f => Applicative f, … aka ‘the Jenga tower’).
Then you can’t define just one or two parametric methods; you’d need parametric versions for the whole Prelude. And with explicit linkages up the hierarchy.
“hard-to-diagnose overloading behaviour” would then be figuring out whether your program parametrically chose an instance vs ad-hoc inferred, and whether that was what you intended.
(As I said above, not better nor worse, just confusingly different.)
I don’t mean to imply that doing the “type classes parametrically” is a good idea in Haskell. It was just to contrast to Agda’s “type class” approach, demonstrating that Agda’s approach works both parametrically and ad-hoc, doing the same two things done in Haskell, just without having to choose between the two. It scales fine because it’s just one approach that does both, rather than two separate approaches that step on each other’s toes.
If introducing systemN +1 means my codebase of 100% systemN becomes 90% systemN and 10% systemN +1 and it gets rid of problems from systemN but systemN +1 has those problems, then I removed those problems from 90% of my codebase.
Given you’re on a Haskell forum, presumably you find value in a type system for your values. So why not a type system for your type system? Even if you have reasons for the former and not the latter, it can’t just be “more code” because (presumably) you find the value of the former to be worth the “more code” that it requires.
If I write an error at value level, but my type level declaration is correct (and applicable to the error), I catch the bug. If my type level declaration also has an error, but my type’s type level declaration is correct (and applicable to the error), I catch the bug. Sounds like redundancy to me.
If introducing systemN +1 means my codebase of 100% systemN becomes 90% systemN and 10% systemN +1 and it gets rid of problems from systemN but systemN +1 has those problems, then I removed those problems from 90% of my codebase.
“Type” system level
fraction of errors not found
1
10% (0.1)
2
1% (0.12 = 0.01)
3
0.1%
4
0.01%
…therefore no matter how many levels there are, some bugs will always remain undetected. So again:
…which I’ll rewrite as:
If you write an error at value level, but your typeN -level declaration is correct (and applicable to the error), you catch the bug.
If your typeN -level declaration also has an error, but your typeN’s typeN +1 -level declaration is correct (and applicable to the error), you catch the bug.
Sounds like redundancy to me.
Here’s the definition of “redundancy” I’m relying on:
But if you have a tower of N -1 sufficiently-featured type systems and the fragments of one more, then the loss of only one type system is enough for source-code bugs to be missed. Therefore the entire tower has to work! Or using the avionics example, all of the computers must work for the aircraft to keep flying safely (no redundancy).
Fortunately, aircraft everywhere use the dictionary definition of “redundancy” for their avionic systems - if only one system fails, the pilots probably still can land their aircraft safely.
Given you’re on a Haskell forum, presumably you find value in a type system for your values.
Conditionally - I also agree with the concept of diminishing returns, with a bemusing example provided by roundabouts; this being an ordinary one:
That’s a “roundabout of roundabouts” - five small ones arranged in a loop (appearing as white dots amongst the vehicles) around a large one in the middle (the white dot in the middle of the central circular area). As you can now probably understand, there are very few of these anywhere in the world: going beyond a single roundabout at an intersection of roads provides diminishing returns, but so much added complexity, and extra “fun” for learner-drivers!
So far this topic has attracted over 200 “likes”, mostly for “pro-DT” posts. So if even 10% of those individual “likers” (approximately 20 people) were to join int-index and sand-witch in this experiment, we (including Haskell educators and practitioners) will all be able to see the results that much faster.
Why the emphasis on educators and practitioners? Because we want more people using Haskell, not less:
educators teaching more students Haskell, who then go on to be practitioners;
practitioners advocating for the use of Haskell, including to prospective students.
So by it arriving more quickly, we’ll have the opinions of educators and practitioners about a “dependent Haskell” that much sooner, and know if this experiment is a success (or not) and respond accordingly.
Identifying an instance in which something isn’t redundant doesn’t invalidate the ways in which it is.
Yes, diminishing returns of course mean that at some point, going further stops being worthwhile. This is an extremely well understood concept. Pointing out the existence of diminishing returns contributes nothing towards the actual difficult part: finding when it is no longer worthwhile.
Identifying an instance in which something isn’t redundant doesn’t invalidate the ways in which it is.
But it does invalidate your counter-example of data corruption:
Pointing out the existence of diminishing returns contributes nothing towards the actual difficult part: finding when it is no longer worthwhile.
If new features and extensions for Haskell tend to benefit experienced users (such as implementors of Haskell) at the expense of making Haskell more difficult to teach, or advocate to future Haskellers, then there simply will be less Haskellers in the future.
So will dependent types be one such addition? I don’t know. Hence me referring to their addition to Haskell as an experiment, and me wanting to know what happens next if that experiment fails since failure is always an option for any experiment:
…and choosing to think wishfully about the risk of failure does exactly nothing to lessen or remove it.
But we’ll all discover if it is a failure or not much more quickly if more people help int-index and sand-witch…
Now hang on. DataKinds arrived 2012. Are we saying that also counts in Dependent Haskell? Then when did DepH start? And what type-system extensions in Haskell post-98 count as non-DepH? We’re losing focus. I think I can be in favour of DataKinds without swallowing the whole DepH kool-aid.
Given GHC’s type system as at 2010, what would be far more valuable to deliver next would be a type system to catch divide-by-zero or numeric overflow or off-by-one errors. A type system for my type system not so much of a priority. (And writing a PolyKinded Typeable to save a handful of different arity Typeables strikes me as thin motivation.)
Note that Oleg’s work used the type system as at 2004. DataKinds are more elegant, but no more expressive than 2004. Note also that Hugs’ extensible records system (TRex ~1996) exploits the implicit kind system (row is a different kind vs *) without anyone needing to write explicit kind signatures. Has GHC three decades on produced a record system? Is DepH going to enable me to produce one? Lenses requires a vast amount of eye-watering code (and was also delivered before DepH – will DepH help Lenses avoid all that Template Haskell?).
I suspect there are a smaller and smaller set of applicable fragments as you go up the hierarchy. So perhaps it’s reasonable for Agda to leave the levels explicit. I note the violence DepH is doing to Haskell to be able to put types in terms. I suspect there’ll be more violence when it comes to writing type-level functions, because of all the syntax from term-level that doesn’t make sense at type-level. IOW when you write a function, you’ll have to know whether this is to be called at levelN vs levelN+1 etc. So the terms vs types vs kinds vs sorts distinction will reappear.
For example: do typeclasses/overloading make sense at the kind level? instance Eq Type ... anyone? Merely testing for the equality of two types without signalling to type inference these types are unifiable will lead to a healthy new source of bugs. if (type a) == (type b) then ... else .... I’d be especially interested in what dragons we can find in the else ... branch.
Now hang on. DataKinds arrived 2012. Are we saying that also counts in Dependent Haskell? Then when did DepH start?
Notice my use of the word “fragments” with regards to the use of “higher” type systems - all “printed” versions of Haskell (from version 1.0 through to 98 and 2010) rely on such artefacts, namely the kind and sort system fragments mentioned here:
By themselves those fragments are relatively benign. Instead, the risk arises from their ongoing extension - what was a fragment now begins to resemble a whole extra type system, with all of the usual problems any type system has. Hence step 3 of that perpetual cycle:
