This is a pernicious, odious, and fundamental misunderstanding about what “totality” actually means. If we are only ever interested in the extensional logical content of code, then sure totality means we’re free to ignore evaluation order. However: (1) That is a conditional argument, not a tautology. (2) The bulk of the consequent follows precisely from the premise that we will never evaluate the code, ergo evaluation order is vacuous. (3) And for some reason I’ve only ever seen folks making this argument in specific circumstances where the premise is known to be false. If someone wants to write programs (i.e., code that gets run), then evaluation order is crucial because it determines whether the code is adequate to perform whatever it is the program should do and the constraints under which it should do them (execution time, resource usage, etc). Unlike proofs, programs fundamentally incorporate evaluation properties that are not captured by the extensional logical content of the code implementing them. (This too is fundamental: if we had a language that incorporated all those evaluation properties, then it would be useless for discussing extensional logical equivalence —precisely because it captures those evaluation details which we would like to be abstracting away.)
Whenever someone brings up the idea of “Lazy Agda”, it is because they are wanting to use “Agda” as a language for writing programs rather than as a language for writing proofs. Retorting that “Agda is total and therefore evaluation order is meaningless” is intentionally misinterpreting what that person is saying.
I have no horse in the evaluation strategy race, but as a matter of rhetoric, you’re more likely to persuade hearts and minds, to say nothing of protecting your own social capital, if you stick to the facts rather than imputing bad faith to anyone.
Pardon my ignorance, but I don’t understand where you are disagreeing with me. The very first part of my argument (that you chose not to quote) is that you cannot “run” Agda unless you extract Haskell code, which is lazy. Basically lazy Agda.
Only then do I make an argument that unless you want to run a program, evaluation order does not matter (much). This is all to refute the repeated claim that Agda is currently a strict language that somehow needs to have a lazy variant so that proponents of dependent Haskell can just use lazy Agda and let Haskell stay Haskell2010.
As for me, there are two reasons why I’ve suggested the addition of laziness to Adga:
The length of time needed to transition to a dependent Haskell (but int-index’s task-breakdown page ought to reduce that time drastically, having seen the mass “liking” of posts here which are favour of dependent types :-).
The possibility of a future dependent Haskell being total, with the subsequent temptation to then be strict by default:
and rely entirely on purity to keep effects in check:
But by themselves, purity and its benefits - referential transparency, ease of parallelism, etc - aren’t having much success elsewhere:
So purity and laziness work better together than apart. Moreover, laziness usually implies purity:
…which now has to be the only reason why anyone can still proclaim “I/O is pure” in Haskell, or “Haskell is purely functional” - without Haskell’s non-strict semantics, such statements would be that much easier to refute.
So instead of adding dependent types to the last remaining widely-supported non-strict language, make Agda into another non-strict language with similar support - if lazy Agda fails, at least there’ll still be non-dependent Haskell…
I’ve started to think of Haskell as a family of languages which each take plus or minus some things from a grab bag of familiar language features, like purity, but crucially a vocabulary (fold, scan, etc) that is reusable in the libraries with a mostly familiar syntax. Glasgow Haskell, Elm, PureScript, Hell, Unison, Roc, Idris. I don’t have to work too hard to think in each of these. That’s a great achievement.
I think it’s not worth competing with GHC as a general purpose Haskell, because it has both the language extensions and the industry grade runtime, with the package ecosystem, so naturally it’s more rewarding to put everything (linear types, dependent type, arrows???, etc) into GHC.
I think it’s possible and practical to do a reset and carve out a niche that Glasgow Haskell doesn’t do well (and maybe doesn’t want to do well), like the other languages I listed. I can give you a clean and simple frontend language (Elm) in exchange for dropping all your beloved language features—many people say, great! (Or give me PureScript.) I could imagine e.g. a simpler Haskell that performs well but compiles lightning fast like Go—that would be worth it for some people in industry where compile times are agony. Maybe Unison or Roc will someday be that.
So for that reason though I don’t personally think much of dependent types (compared to other types of software verification), I kind of accept it as part of the trade off that I also get to greedily pounce on my pet features, that some other people don’t like or care about, every other GHC release, produced and distributed to me as free software.
…and as a result both extensions can now only be accessed by using the appropriate command-line options in GHC. But dependent types are different - to many here, "they are the future of Haskell" and (eventually) there won’t be a option to disable them. So if you don’t like dependent types, or just have some doubts about them:
…well that’s just too bad. But there supposedly are plenty of other languages to choose from!
(If you’re content with strict semantics.)
Don’t understand this point. [to echo sgraf’s reaction. And Good grief! why didn’t I comment on this claim at the time?]
An important feature of type families/especially associated TFs is that they’re extensible. They fit in with extensible type classes and the module system and separate compilation[**]. Somebody can import my typeclass with its Assoc TF’s; declare their own data types; declare instances of the class and TFs.
Presuming DH’s ‘Dependent Functions’ are like term-level functions, we can’t write open-ended type case. (Also I don’t see what’s hard to grasp about the individual instances of Assoc TFs; they already look a lot like functions.)
What is maybe hard to grasp about Assoc TFs is the ‘distributed logic’ of having instances in many modules/where each data type is declared. But the compiler helps us there: Assoc TF instances can’t overlap/if you want overlap you must use a Closed TF with all its logic in one place.
Now you might say FunDeps are a complex part of Haskell (that is, how they interact across different instances). (Assoc) TFs have already relieved that. So I’m plain not seeing why/how Dependent Haskell will make anything “simpler”.
[**] And follow-up q: I see Agda doesn’t have a thing called ‘type class’, although it does have an overloading mechanism. Does that mechanism count as part of Dependent Typing, or is it an orthogonal feature? How does it fit with modules and separate compilation? Are overlapping instances allowed? If not, how to implement the (fairly frequent) use cases for overlap in Haskell?
In a thread off-forum, we rather came to the conclusion that if you didn’t have type classes, you’d need to invent them (or something practically indistinguishable, including overlaps) to get the power we have in Haskell.
My point was: If you want a closed type family, you actually want a type-level function. If you want an open type family, (I will question your design, and) you can often replace it with an associated type/type method of a type class. Note that although GHC chooses to compile associated types similarly to open type families, that need not be the case. For example, in a dependently-typed language, an associated type of a type class is simply a type-valued method, as I exemplify below using Haskell syntax:
type family F a b :: Type
type instance F Int Char = Bool
...
==>
class C a b where
f :: Type
instance C Int Char where
f = Bool
...
(Yes, would need -XAmbiguousTypes. Can be worked around with some of the visible forall improvements that are ongoing, I think.)
Now the evidence for a C Int Char constraint contains means to concoct a proof for f @Int @Char ~ Bool, similar to F Int Char ~ Bool in the original program (although I’m not sure if Dependent Haskell would in practice choose to represent definitional equality as coercion axioms.)
I’ve always taken it from the get go (2008) that Type Families are functions at the type level. The implementers chose not to call them “functions” (but did choose a name starting f) because:
Many of the constructs you can use in term-level expressions make no sense in types.
TFs must be ‘evaluated’/reduced at compile time, so that type inference/checking/instance selection can complete.
I’m pretty sure you’re wrong there: all the docos say an Assoc type decl is simply alternative syntax for a Type Family. “A data or type synonym family can be declared as part of a type class” [quoting from the section linked below]. If you think they’re two different things, then you’ve over-complicated it, and your “simpler” claim above is merely because you haven’t realised Assoc types simply are TFs.
Again I disagree: open TFs/equivalently Assoc types are the replacement for FunDeps. They must be open because class/instances are open, so FunDeps are open. Again you’re describing the existing situation as more complex than it is, and Dependent Typing is no simpler.
You perhaps think TFs can’t be like functions because they’re spelled upper-case. That was a stupid design choice: everything else spelled upper-case in Haskell is injective. If I had a penny for every time I thought I was looking at a type only to realise it’s a TF call …
There’s nothing “simply” about a method that has to return a type not a value and be able to do that statically at compile time. Its arguments also have to be (interpreted as) types, for example.
That example is crying out for a FunDep. Think of a FunDep as simply a type-valued method; but placed syntactically in the class/instance header so you can see what its arguments are. Also why isn’t f declared like a sensible method?
class C a b where
someMeth :: a -> b -> f a b -- f has arguments, doesn't it?
f :: a -> b -> Type -- so it needs a signature to show that [**]
instance C Int Char where
someMeth x y = last (show x) == y
f _ _ = Bool -- [**]
[**] Oh, but the arguments to f-qua-method in its signature can’t be named as a b because in a method signature that denotes the type of a term. Never the less, the binding for f within the instance might want to call and pass arguments to some other type-valued function, so it does need a mechanism to name its arguments. Consider for example instance C Int (b1, b2) where ... in which f needs to examine b1 . Or indeed the more complex examples in the docos
6.4.9.4. Associated data and type families
The type parameters must all be type variables, of course, and some (but not necessarily all) of then can be the class parameters. Each class parameter may only be used at most once per associated type, but some may be omitted and they may be in an order other than in the class head.
And why are you calling f using that @ syntax? If you’re telling me it’s simply a type-valued function, why aren’t its arguments simply type-valued expressions (aka Types). And why are you talking about “concoct a proof”? I don’t say “concoct a proof for 1 + 1 ~ 2”, Iff is simply a type-valued function and we’re using function terminology, f Int Char evaluates to Bool.
Remember that I can put a (Assoc) Type Family call f Int Bool in a type/signature anywhere throughout the program, it doesn’t have to be within an instance decl.
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.
) because: